Report Number: CS-TR-99-1618
Institution: Stanford University, Department of Computer Science
Title: Abstraction-based Deductive-Algorithmic Verification of Reactive Systems
Author: Uribe, Tomas E.
Date: March 1999
Abstract: This thesis presents a framework that combines deductive and algorithmic methods for verifying temporal properties of reactive systems, to allow more automatic verification of general infinite-state systems and the verification of larger finite-state ones. Underlying these methods is the theory of property-preserving assertion-based abstractions, where a finite-state abstraction of the system is deductively justified and algorithmically model checked. After presenting an abstraction framework that accounts for fairness, we describe a method to automatically generate finite-state abstractions. We then show how a number of other verification methods, including deductive rules, (Generalized) Verification Diagrams, and Deductive Model Checking, can also be understood as constructing finite-state abstractions that are model checked. Our analysis leads to a better classification and understanding of these verification methods. Furthermore, it shows how the different abstractions that they construct can be combined. For this, we present an algorithmic Extended Model Checking procedure, which uses all the information that these methods produce, in a finite-state format that can be easily and incrementally combined. Besides a standard safety component, the combined abstractions include extra bounds on fair transitions, well-founded orders, and constrained transition relations for the generation of counterexamples. Thus, our approach minimizes the need for user interaction and maximizes the impact of the available automated deduction and model checking tools. Once proved, verification conditions are re-used as much as possible, leaving the temporal and combinatorial reasoning to automatic tools.
http://i.stanford.edu/pub/cstr/reports/cs/tr/99/1618/CS-TR-99-1618.pdf