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...

• Type: Conference
• Year: 1999
• Where: CAV
• Authors: Orna Kupferman, Moshe Y. Vardi
• Keywords: CAV 1999, General Linear Property, Hardware, Model Checking, Safety Properties