Journal article
Verification by augmented abstraction: The automata-theoretic view
Journal of Computer and System Sciences, Vol.62(4), pp.668-690
Jun/2001
Abstract
This paper deals with the proof method of verification by finitary abstraction (VFA), which presents an alternative approach to the verification of (potentially infinite-state) reactive systems. We assume that the negation of the property to be verified is given by the user in the form of an infinite-state nondeterministic Buchi discrete system (BDS). The method consists of a two-step process by which, in a first step. the system and its (negated) specification are combined into a single infinite-state fair discrete system (FDS, which is similar to a BDS but with Streett acceptance conditions), which is abstracted into a finite-state automaton. The second step uses model checking to establish that the abstracted automaton is infeasible. i.e.. has no computations. The VFA method can be considered as a viable alternative to verification by temporal deduction, which. up to now, has been the main method generally applicable for verification of infinite-state systems. The paper presents a general recipe for an FDS abstraction, which is shown to be sound. where soundness means that infeasibility of the abstracted FDS implies infeasibility of the unabstracted one, implying in turn the validity of the property over the concrete (infinite-state) system. To make the method applicable for the verification of liveness properties, pure abstraction is sometimes no longer adequate. We show that by augmenting the system with an appropriate (and standardly constructible) progress monitor. we obtain an augmented system, whose computations are essentially the same as those of the original system and which may now be abstracted while preserving the desired liveness properties. We refer to the extended method as verification by augmented abstraction (VAA). We then proceed to show that the VAA method is sound and complete fur proving all properties: whose negations are expressible by a sus. Given that every linear temporal logic (LTL) property can be translated to a BDS this establish
Details
- Title
- Verification by augmented abstraction; The automata-theoretic view
- Creators
- Y Kesten (null)Amir Pnueli (null) - The Weizmann Institute of ScienceMY Vardi (null)
- Resource Type
- Journal article
- Publication Details
- Journal of Computer and System Sciences, Vol.62(4), pp.668-690; Jun/2001
- Number of pages
- 23
- Language
- English
- DOI
- https://doi.org/10.1006/jcss.2000.1744
- Scientific Unit
- The Weizmann Institute of Science
- Record Identifier
- 993264942703596
Metrics
6 Record Views