Model Checking of Safety Properties

10 years 8 months ago
Model Checking of Safety Properties
Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. A computation that violates a general linear property reaches a bad cycle, which witnesses the violation of the property. Accordingly, current methods and tools for model checking of linear properties are based on a search for bad cycles. A symbolic implementation of such a search involves the calculation of a nested fixed-point expression over the system’s state space, and is often very difficult. Every computation that violates a safety property has a finite prefix along which the property is violated. We use this fact in order to base model checking of safety properties on a search for finite bad prefixes. Such a search can be performed using a simple forward or backward symbolic reachability check. A naive methodology that is based on such a search involves a construction of an automaton (or a tableau) that is doubly exponential in the pro...
Orna Kupferman, Moshe Y. Vardi
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where CAV
Authors Orna Kupferman, Moshe Y. Vardi
Comments (0)