Principles of Model Checking: Difference between revisions
DavidGries (talk | contribs) →Synopsis: Changed links to "safety" and "liveness" because those page may be retired in favor of the page "Safety and liveness properties" Tag: Reverted |
m Disambiguating links to Deadlock (link changed to Deadlock (computer science)) using DisamAssist. |
||
| (3 intermediate revisions by 3 users not shown) | |||
| Line 15: | Line 15: | ||
==Synopsis== |
==Synopsis== |
||
[[File: |
[[File:2-state Buchi automaton.svg|thumb|alt=Buchi automaton|An example [[transition system]] used to model a process]] |
||
The introduction and first chapter outline the field of [[model checking]]: a model of a machine or process can be analysed to see if desirable properties hold. For instance, a [[vending machine]] might satisfy the property "the balance can never fall below €0,00". A video game might enforce the rule "if the player has 0 lives then the game ends in a loss". Both the vending machine and video game can be modelled as [[transition system]]s. Model checking is the process of describing such requirements in mathematical language, and automating proofs that the model satisfies the requirements, or discovery of [[counterexample]]s if the model is faulty. |
The introduction and first chapter outline the field of [[model checking]]: a model of a machine or process can be analysed to see if desirable properties hold. For instance, a [[vending machine]] might satisfy the property "the balance can never fall below €0,00". A video game might enforce the rule "if the player has 0 lives then the game ends in a loss". Both the vending machine and video game can be modelled as [[transition system]]s. Model checking is the process of describing such requirements in mathematical language, and automating proofs that the model satisfies the requirements, or discovery of [[counterexample]]s if the model is faulty. |
||
The second chapter focuses on creating an appropriate model for [[concurrency (computer science)|concurrent systems]], where multiple parts of an [[algorithm]] (set of instructions) can be carried out simultaneously by different machines or parts of a machine. |
The second chapter focuses on creating an appropriate model for [[concurrency (computer science)|concurrent systems]], where multiple parts of an [[algorithm]] (set of instructions) can be carried out simultaneously by different machines or parts of a machine. |
||
Chapters 3 explores types of rules that a transition system may satisfy: [[linear time properties]]. A [[ |
Chapters 3 explores types of rules that a transition system may satisfy: [[linear time properties]]. A [[safety property]], such as "no [[Deadlock (computer science)|deadlock]] states are possible", is of the form "an undesirable outcome can never occur". A [[liveness]] property, such as "a shared resource will always eventually be made available to a component that requests it", is of the form "a desirable outcome will eventually happen". Fairness properties such as "a traffic light never stops changing colour" can be used as [[precondition]]s i.e. assumptions from which other properties can be deduced. |
||
The fourth chapter is about [[regular language|regular]] and [[Omega-regular language|ω-regular]] language properties, and theoretical machines such as [[Büchi automata]] that model the languages. It gives model-checking algorithms to verify properties or find counterexamples. |
The fourth chapter is about [[regular language|regular]] and [[Omega-regular language|ω-regular]] language properties, and theoretical machines such as [[Büchi automata]] that model the languages. It gives model-checking algorithms to verify properties or find counterexamples. |
||
| Line 42: | Line 42: | ||
==External links== |
==External links== |
||
* [https://mitpress.mit.edu/ |
* [https://mitpress.mit.edu/9780262026499/principles-of-model-checking/ Official website] |
||
[[Category:2008 non-fiction books]] |
[[Category:2008 non-fiction books]] |
||
Latest revision as of 21:30, 20 August 2024
 Front cover | |
| Author | Christel Baier and Joost-Pieter Katoen |
|---|---|
| Subject | Model checking |
| Publisher | MIT Press |
Publication date | 25 April 2008 |
| Pages | 975 |
| ISBN | 9780262026499 |
Principles of Model Checking is a textbook on model checking, an area of computer science that automates the problem of determining if a machine meets specification requirements. It was written by Christel Baier and Joost-Pieter Katoen, and published in 2008 by MIT Press.
Synopsis
[edit]
The introduction and first chapter outline the field of model checking: a model of a machine or process can be analysed to see if desirable properties hold. For instance, a vending machine might satisfy the property "the balance can never fall below €0,00". A video game might enforce the rule "if the player has 0 lives then the game ends in a loss". Both the vending machine and video game can be modelled as transition systems. Model checking is the process of describing such requirements in mathematical language, and automating proofs that the model satisfies the requirements, or discovery of counterexamples if the model is faulty.
The second chapter focuses on creating an appropriate model for concurrent systems, where multiple parts of an algorithm (set of instructions) can be carried out simultaneously by different machines or parts of a machine.
Chapters 3 explores types of rules that a transition system may satisfy: linear time properties. A safety property, such as "no deadlock states are possible", is of the form "an undesirable outcome can never occur". A liveness property, such as "a shared resource will always eventually be made available to a component that requests it", is of the form "a desirable outcome will eventually happen". Fairness properties such as "a traffic light never stops changing colour" can be used as preconditions i.e. assumptions from which other properties can be deduced.
The fourth chapter is about regular and ω-regular language properties, and theoretical machines such as Büchi automata that model the languages. It gives model-checking algorithms to verify properties or find counterexamples.
The fifth and sixth chapters explore linear temporal logic (LTL) and computation tree logic (CTL), two classes of formula that express properties. LTL encodes requirements about paths through a system, such as "every Monopoly player passes 'Go' infinitely often"; CTL encodes requirements about states in a system, such as "from any position, all players can eventually land on 'Go'". CTL* formulae, which combine the two grammars, are also defined. Algorithms for model-checking formulae in these logics are given.
The seventh chapter explores formal ways to compare transition systems, such as bisimulation; the eighth is about partial order reductions that aim to reduce the computation required to verify properties of a model. The ninth and tenth chapters are about extensions to the logics and automata previously considered, including through addition of a clock speed (timed automata) or probabilities (probabilistic automata, based on Markov chains).
Reception
[edit]François Laroussinie, writing in The Computer Journal, recommended the book to researchers, lecturers, students and engineers, calling the book "impressive". Laroussinie found the textbook comprehensive and accessibly written, with a good number of examples, exercises and motivating ideas for key concepts. With a "unified framework", the first seven chapters cover classical theory and the last three chapters cover extensions of model checking.[1]
In ACM Computing Reviews, Gabriel Ciobanu believed the textbook could be used in advanced undergraduate or graduate courses, and would be useful to researchers. Ciobanu praised the "clear and intuitive" presentation and said it "should be appreciated for its pedagogical approach to covering basic concepts, deep theoretical results, and advanced topics in model checking research".[2]
In 2014, the book was one of the five most-cited academic texts monitored by the Book Citation Index (BKCI).[3]
References
[edit]- ^ Laroussinie, François (2010). "Principles of Model Checking (Review)". The Computer Journal. 53 (5): 615–616. doi:10.1093/comjnl/bxp025.
- ^ Ciobanu, Gabriel (8 January 2009). "Principles of Model Checking (Review)". ACM Computing Reviews.
- ^ Kousha, Kayvan; Thelwall, Mike (1 March 2016). "Can Amazon.com Reviews Help to Assess the Wider Impacts of Books?". Journal of the Association for Information Science and Technology: 580.
Further reading
[edit]- Lange, Martin (2010), MathSciNet, MR 2493187
{{citation}}: CS1 maint: untitled periodical (link)