What do you think?
Rate this book
Principles of Model Checking
A comprehensive introduction to the foundations of model checking, a fully automated technique for finding flaws in hardware and software; with extensive examples and both practical and theoretical exercises. Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.
975 pages, Hardcover
First published April 25, 2008
7 people are currently reading
141 people want to read
Ratings & Reviews
Friends & Following
Create a free account to discover what your friends think of this book!
Community Reviews
Displaying 1 - 5 of 5 reviews
December 19, 2017
Very good book about automated model checking from first principles. A must-read for everybody who wants to know more on the topic. For the more pragmatic engineer who wants to use model checking this may be overkill although a better understanding of the technology will probably lead to better models or less frustration while building and running models.
Examples use (a subset of) Promela/SPIN and there's a bibliographic reference to Leslie Lamport's TLA+.
Examples use (a subset of) Promela/SPIN and there's a bibliographic reference to Leslie Lamport's TLA+.
March 10, 2022
This year, one of my reading theme is to understand what is "correctness":
- [How traditional reasoning does it] Formal logic (e.g., history of logic, history of math, history of formal language)
- [How CS does it] Program verification (also related to model theory, formal language theory)
- [How NLP does it] Some good-faith heuristics (e.g., CheckList, adversarial attack)
From this book, I learned the profound concept of model checking for CS (so the second thread above).
1) Mind-changing point: We already know that humans make errors, but it is astounding to know that even computer systems that we take as granted often have errors too. Nothing works perfectly correctly as we thought :).
This profoundness spans across (a) the philosophical question of what is correctness and how can humans approach it, (b) the study of logic and math of how to manually check correctness, (c) the study of CS of how to automatically check it, (d) practical concerns that balance among cost, use case, and reliability.
2) Use cases & guiding principles
- We want to use the power of automation, e.g., planes
- But we do not want to have fatal errors, e.g., malfunction of the algorithms in the plane causing it to crash.
There is a tradeoff similar to the precision-recall curve. If we do not want any machine errors, some people can choose to abandon the machines, and fully turn to manual decisions. Admittedly, humans could also make more errors than machines, although the ethical concerns are totally different.
As a result, we aim to reach a balance: We want "usable" machines, with "tolerable" errors both functionally and practical by our "budget" to verify/improve it. Overall the machines need to do more good than harm, and within the ethical toleration of our society.
Note: Nobody has infinite budget to improve the machine to the perfect correctness. We always aim at a balance point.
Examples in the book: "The fatal defects in the control software of the Ariane-5 missile (Figure 1.1), the Mars Pathfinder, and the airplanes of the Airbus family led to headlines in newspapers all over the world and are notorious by now. A software flaw in the control part of the radiation therapy machine Therac-25 caused the death of six cancer patients between 1985 and 1987 as they were exposed to an overdose of radiation."
3) Goal of this subject: "establish system correctness with mathematical rigor."
Verification techniques:
- exhaustive exploration (model checking)
- experiments with a restrictive set of scenarios in the model (simulation), or in reality (testing)
Ideal test (extrinsic): exhaustive testing of all execution paths (which is practically infeasible) and all possible input-output pairs of these execution paths.
Ideal test (intrinsic): logical verification
- practical workarounds:
-- peer review (which catches between 31 % and 93 % of the defects with a median around 60%)
-- before writing the system: the designers should be trained to be aware of certain principles.
Practical scenarios:
- Use an ensemble of practices, e.g., combine peer review and testing which catch different classes of defects at different stages in the development cycle.
Common properties to verify for computer systems:
- functional correctness (does the system do what it is supposed to do?),
- reachability (is it possible to end up in a deadlock state? i.e., a system should never be able to reach a situation in which no progress can be made)
- safety (“something bad never happens”)
- liveness (“something good will eventually happen”)
- fairness (does, under certain conditions, an event occur repeatedly?)
- and real-time properties (is the system acting in time?).
- invariants,
- request-response properties.
4) Deep problems:
What do we check the program against?
a) Against some oracle pairs of input and outputs?
b) Against some principles that we design?
- "the formalization of all system properties for a subset of the ISDN user part protocol revealed that 55% (!) of the original, informal system requirements were inconsistent."
- the property specification prescribes what the system should do, and what it should not do,
- the model description addresses how the system behaves.
- The model checker examines all relevant system states to check whether they satisfy the desired property. If a state is encountered that violates the property under consideration, the model checker provides a counterexample that indicates how the model could reach the undesired state. The counterexample describes an execution path that leads from the initial system state to a state that violates the property being verified. With the help of a simulator, the user can replay the violating scenario, in this way obtaining useful debugging information, and adapt the model (or the property) accordingly.
== Key philosophical question ==
Verification and validation should not be confused. Verification amounts to check that the design satisfies the requirements that have been identified, i.e., verification is “check that we are building the thing right”. In validation, it is checked whether the formal model is consistent with the informal conception of the design, i.e., validation is “check that we are verifying the right thing”
Are we able to check whether we are verifying the right thing, or even express what is the right thing accurately/formally?
- [How traditional reasoning does it] Formal logic (e.g., history of logic, history of math, history of formal language)
- [How CS does it] Program verification (also related to model theory, formal language theory)
- [How NLP does it] Some good-faith heuristics (e.g., CheckList, adversarial attack)
From this book, I learned the profound concept of model checking for CS (so the second thread above).
1) Mind-changing point: We already know that humans make errors, but it is astounding to know that even computer systems that we take as granted often have errors too. Nothing works perfectly correctly as we thought :).
This profoundness spans across (a) the philosophical question of what is correctness and how can humans approach it, (b) the study of logic and math of how to manually check correctness, (c) the study of CS of how to automatically check it, (d) practical concerns that balance among cost, use case, and reliability.
2) Use cases & guiding principles
- We want to use the power of automation, e.g., planes
- But we do not want to have fatal errors, e.g., malfunction of the algorithms in the plane causing it to crash.
There is a tradeoff similar to the precision-recall curve. If we do not want any machine errors, some people can choose to abandon the machines, and fully turn to manual decisions. Admittedly, humans could also make more errors than machines, although the ethical concerns are totally different.
As a result, we aim to reach a balance: We want "usable" machines, with "tolerable" errors both functionally and practical by our "budget" to verify/improve it. Overall the machines need to do more good than harm, and within the ethical toleration of our society.
Note: Nobody has infinite budget to improve the machine to the perfect correctness. We always aim at a balance point.
Examples in the book: "The fatal defects in the control software of the Ariane-5 missile (Figure 1.1), the Mars Pathfinder, and the airplanes of the Airbus family led to headlines in newspapers all over the world and are notorious by now. A software flaw in the control part of the radiation therapy machine Therac-25 caused the death of six cancer patients between 1985 and 1987 as they were exposed to an overdose of radiation."
3) Goal of this subject: "establish system correctness with mathematical rigor."
Verification techniques:
- exhaustive exploration (model checking)
- experiments with a restrictive set of scenarios in the model (simulation), or in reality (testing)
Ideal test (extrinsic): exhaustive testing of all execution paths (which is practically infeasible) and all possible input-output pairs of these execution paths.
Ideal test (intrinsic): logical verification
- practical workarounds:
-- peer review (which catches between 31 % and 93 % of the defects with a median around 60%)
-- before writing the system: the designers should be trained to be aware of certain principles.
Practical scenarios:
- Use an ensemble of practices, e.g., combine peer review and testing which catch different classes of defects at different stages in the development cycle.
Common properties to verify for computer systems:
- functional correctness (does the system do what it is supposed to do?),
- reachability (is it possible to end up in a deadlock state? i.e., a system should never be able to reach a situation in which no progress can be made)
- safety (“something bad never happens”)
- liveness (“something good will eventually happen”)
- fairness (does, under certain conditions, an event occur repeatedly?)
- and real-time properties (is the system acting in time?).
- invariants,
- request-response properties.
4) Deep problems:
What do we check the program against?
a) Against some oracle pairs of input and outputs?
b) Against some principles that we design?
- "the formalization of all system properties for a subset of the ISDN user part protocol revealed that 55% (!) of the original, informal system requirements were inconsistent."
- the property specification prescribes what the system should do, and what it should not do,
- the model description addresses how the system behaves.
- The model checker examines all relevant system states to check whether they satisfy the desired property. If a state is encountered that violates the property under consideration, the model checker provides a counterexample that indicates how the model could reach the undesired state. The counterexample describes an execution path that leads from the initial system state to a state that violates the property being verified. With the help of a simulator, the user can replay the violating scenario, in this way obtaining useful debugging information, and adapt the model (or the property) accordingly.
== Key philosophical question ==
Verification and validation should not be confused. Verification amounts to check that the design satisfies the requirements that have been identified, i.e., verification is “check that we are building the thing right”. In validation, it is checked whether the formal model is consistent with the informal conception of the design, i.e., validation is “check that we are verifying the right thing”
Are we able to check whether we are verifying the right thing, or even express what is the right thing accurately/formally?
February 13, 2020
I read only first 7 chapters for exams, and the last chapter on Markov chain for knowledge.
I like the length they went through to keep the same examples across the book, so you develop a sort of aspects and approach towards the space of model checking. Really good versed and carries you with it to see the algorithms with minimal distortions on intuitions.
-Will be getting back to it from time to time to brush up.
-Good and complete book on the topic.
I like the length they went through to keep the same examples across the book, so you develop a sort of aspects and approach towards the space of model checking. Really good versed and carries you with it to see the algorithms with minimal distortions on intuitions.
-Will be getting back to it from time to time to brush up.
-Good and complete book on the topic.
June 4, 2022
This is something I read some time ago- it probably wasn't the right choice of title. IIRC a long time ago, I read the Handbook of Model Checking- which was unfortunately taken from my flat, part way through reading it. Edmund Clarke's introduction, which is in, it's 2nd edition, I do find a bit more useful.
December 20, 2008
great book for model checkign,no doubt.
Displaying 1 - 5 of 5 reviews