model checking
≈ 4 min read
Names in other languages
- PortuguêsVerificação de modelos
- skOverovanie modelov
- ΕλληνικάΈλεγχος μοντέλων
- РусскийПроверка моделей
- DeutschModel Checking
- Englishmodel checking
- FrançaisModel checking
- Tiếng ViệtModel checking
- 日本語モデル検査
Article bodies are English and are not machine-translated. A name in another language is not a translation of the article.
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 th floor's call button is pressed, the cabin will eventually stop at the n th 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.
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 th floor's call button is pressed, the cabin will eventually stop at the n th 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. ===Example=== 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: \begin{align}\Box\Big((\texttt{call} \land \Diamond \texttt{open}) \to & \big((\lnot \texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\ & (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U}\\ & (\texttt{open} \lor ((\lnot \texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\ & (\texttt{open} \lor ((\texttt{atfloor} \land \lnot \texttt{open}) ~\mathcal{U} \\ & (\texttt{open} \lor (\lnot \texttt{atfloor} ~\mathcal{U}~ \texttt{open}))))))))\big)\Big)\end{align} Here, \Box should be read as "always", \Diamond as "eventually", \mathcal{U} as "until" and the other symbols are standard logical symbols, \lor for "or", \land for "and" and \lnot for "not". ==See also==
Text derived from https://en.wikipedia.org/w/index.php?oldid=1374065854 under CC BY-SA 4.0; modifications have been made.