Model checking. (English) Zbl 0847.68063
Broy, Manfred (ed.), Deductive program design. Proceedings of the NATO Advanced Study Institute, Marktoberdorf, Germany, July 26–August 7, 1994. Berlin: Springer-Verlag. NATO ASI Ser., Ser. F, Comput. Syst. Sci. 152, 305-349 (1996).
Summary: Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a state-transition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications.
This paper describes the basic model checking algorithm and shows how it can be used with binary decision diagrams to verify properties of large state-transition graphs. Abstraction and compositional reasoning techniques are also discussed that significantly extend the power of model checking techniques by exploiting the hierarchical structure of complex circuit designs and protocols.
For the entire collection see [Zbl 0842.00044].
This paper describes the basic model checking algorithm and shows how it can be used with binary decision diagrams to verify properties of large state-transition graphs. Abstraction and compositional reasoning techniques are also discussed that significantly extend the power of model checking techniques by exploiting the hierarchical structure of complex circuit designs and protocols.
For the entire collection see [Zbl 0842.00044].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
