Model checking

Elevator control software can be model-checked to verify both safety properties, like "The cabin never moves with its door open", and liveness properties, like "Whenever the n floor's call button is pressed, the cabin will eventually stop at the n floor and open the door".

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash).

In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language. To this end, the problem is formulated as a task in logic, namely to check whether a structure satisfies a given logical formula. This general concept applies to many kinds of logic and many kinds of structures. A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure.

M with initial state M is finite, as it is in hardware, model checking reduces to a graph search.

Instead of enumerating reachable states one at a time, the state space can sometimes be traversed more efficiently by considering large numbers of states at a single step. When such state-space traversal is based on representations of a set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic.

Historically, the first symbolic methods used BDDs. After the success of propositional satisfiability in solving the planning problem in artificial intelligence (see satplan) in 1996, the same approach was generalized to model checking for linear temporal logic (LTL): the planning problem corresponds to model checking for safety properties. This method is known as bounded model checking. The success of Boolean satisfiability solvers in bounded model checking led to the widespread use of satisfiability solvers in symbolic model checking.

One example of such a system requirement: Between the time an elevator is called at a floor and the time it opens its doors at that floor, the elevator can arrive at that floor at most twice. The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:

◊ as "eventually", ∧ for "and" and k or fewer steps. This typically involves encoding the restricted model as an instance of SAT. The process can be repeated with larger and larger values of "Amir Pnueli - A.M. Turing Award Laureate".

↑ Queille, J. P.; Sifakis, J. (1982), "Specification and verification of concurrent systems in CESAR", International Symposium on Programming, Lecture Notes in Computer Science, vol. 137, pp. 337–351, doi:10.1007/3-540-11494-7_22, ISBN 978-3-540-11494-9

↑ Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19: 7–34. doi:10.1023/A:1011276507260. S2CID 2484208.

↑ de la Riva, Claudio; Tuya, Javier (2006). "Automatic generation of assumptions for modular verification of software specifications". Journal of Systems and Software. 79 (9): 1324–1340. doi:10.1016/j.jss.2005.11.570. hdl:10651/29644. ISSN 0164-1212.

↑

• Symbolic Model Checking, Kenneth L. McMillan, Kluwer, "CUDD: CU Decision Diagram Package".
• ↑ Dawar, A; Kreutzer, S (2009). "Parameterized complexity of first-order logic" (PDF). ECCC. S2CID 5856640. Archived from the original (PDF) on 2019-03-03.
• ↑ Storm model checker
• ↑ Zing