Deductive Model Checking |
| |
Authors: | Henny B. Sipma Tomás E. Uribe Zohar Manna |
| |
Affiliation: | (1) Computer Science Department, Stanford University, Stanford, CA, 94305 |
| |
Abstract: | We present an extension of classical tableau-based model checking procedures to the case of infinite-state systems, using deductive methods in an incremental construction of the behavior graph. Logical formulas are used to represent infinite sets of states in an abstraction of this graph, which is repeatedly refined in the search for a counterexample computation, ruling out large portions of the graph before they are expanded to the state-level. This can lead to large savings, even in the case of finite-state systems. Only local conditions need to be checked at each step, and previously proven properties can be used to further constrain the search. Although the resulting method is not always automatic, it provides a flexible, general and complete framework that can integrate a diverse number of other verification tools. |
| |
Keywords: | deductive verification model checking reactive systems |
本文献已被 SpringerLink 等数据库收录! |
|