Model checking: | Guide books | ACM Digital Library

Model checkingApril 2000

Authors:
Edmund M. Clarke
Carnegie Mellon Univ., Pittsburgh, PA
,
Orna Grumberg
Technion–Israel Institute of Technology, Haifa, Israel
,
Doron A. Peled
Bell Labs, Murray Hill, NJ

Publisher:

MIT Press
55 Hayward St.
Cambridge
MA
United States

ISBN:978-0-262-03270-4

Published:03 April 2000

Pages:

314

Available at Amazon

Bibliometrics

Abstract

No abstract available.

Cited By

Contributors

Edmund Melson Clarke, Jr.
Carnegie Mellon University
- Publication Years1976 - 2023
- Publication counts235
- Citation count16,253
- Available for Download56
- Downloads (cumulative)70,323
- Downloads (12 months)4,435
- Downloads (6 weeks)639
- Average Downloads per Article1,256
- Average Citation per Article69
View Full Profile
Orna Grumberg
Technion - Israel Institute of Technology
- Publication Years1983 - 2023
- Publication counts138
- Citation count6,702
- Available for Download17
- Downloads (cumulative)18,748
- Downloads (12 months)1,165
- Downloads (6 weeks)175
- Average Downloads per Article1,103
- Average Citation per Article49
View Full Profile
Doron A Peled
Bar-Ilan University
- Publication Years1987 - 2024
- Publication counts142
- Citation count3,493
- Available for Download10
- Downloads (cumulative)2,812
- Downloads (12 months)195
- Downloads (6 weeks)47
- Average Downloads per Article281
- Average Citation per Article25
View Full Profile

Index Terms

Recommendations

Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...
Read More
Model Checking CTL*[DC]
TACAS 2001: Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems

We define a logic called CTL*[DC] which extends CTL* with ability to specify past-time and quantitative timing properties using the formulae of Quantified Discrete-time Duration Calculus (QDDC). Alternately, we can consider CTL*[DC] as extending logic ...
Read More
Modular Model Checking
COMPOS'97: Revised Lectures from the International Symposium on Compositionality: The Significant Difference

In modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...
Read More

Reviewer: Simon John Thompson

Since the inception of computing, and indeed even before computers were first built, there has been interest in using computers to decide mathematical or logical questions. Of course, Go¨dels pioneering work showed that most mathematical theories are undecidable, meaning that no algorithm can decide whether a formula is a theorem of the theory. Simpler logics such as propositional logic are decidable, and it has been a topic of active mathematical research to determine which logics are decidable, and with what complexity. Computer science has had a profound effect on logic, not least in this area. Evolution over time is a characteristic of most computing systems, and thus temporal logics that allow expression of statements like “P will hold eventually” and “Q will hold until P holds” have been valuable for expressing properties of reactive systems of various kinds. Of course, properties like this can be expressed in first-order logic (FOL) with a distinguished variable for time—“P will hold eventually” can be rendered by “for some time t, P(t) holds”—but a temporal logic has two advantages over this explicit representation: Formulas in temporal logic are easier to read, and thus more likely to be used appropriately. Satisfaction for propositional temporal logic is decidable, while full first-order logics are undecidable. Indeed, one can see the enterprise of defining temporal logics as one of describing decidable subsets of FOL. Of particular interest to logically minded computer scientists is the problem of model checking: this is the question of deciding whether a particular structure, representing a system of some sort, has a property, expressed in a temporal logic. Model checking is not only decidable, but for many temporal logics it is also tractable, with systems with more than 10 100 states being amenable to verification. Model checking can thus be seen as fully automated, symbolic testing of systems for properties expressed in temporal logic. The attraction of model checkers is twofold. First, a correct system can have its correctness certified. Second, equally if not more usefully, if a system fails to have a particular property, the model checker will produce a system trace that witnesses this failure. This evidence gives precisely the diagnostic information needed to fix the system, or at least to remedy the problem diagnosed. The witnessing property has provided much of the impetus for model checking, since existing protocols and systems have been shown to be incorrect in precisely this way. Model checking was invented in the early 1980s, and has proven an abundant source of research challenges over the last two decades. Until now, the research literature has been the only source for an introduction to the topic, but this text now provides an excellent alternative. Clarke is one of the pioneers of the subject, and Grumberg and Peled have been central to some later refinements of the topic. Their book provides both a comprehensive introduction to the basics of the field and an overview of the state-of-the-art techniques that have pushed the technology to its current maturity. It also contains a number of useful case studies as well as descriptions of a number of tools for automated model checking. The book contains an exhaustive bibliography and a serviceable index; its only drawback from a teaching or self-study point of view is the lack of exercises. A reader wanting exercises and a slower-paced introduction might therefore want to refer to Huth and Ryan [1], but otherwise this book is to be highly recommended. The authors give a clear introduction in chapter 1, which sets the scene for most of the chapters (apart from a brief treatment of chapters 16 and 17), while chapter 18 reviews further work and gives a timely set of references. Beyond the basic techniques, which are based on semantic tableaus, automata, and fixed-point theory, there are two important questions: How can model checking be implemented efficiently and How can the scope of model checking be extended The most important innovation for efficient model checking was the introduction of binary decision diagrams (BDDs) for symbolic model checking. BDDs give compact, canonical representations of Boolean functions and relations and thus make it easier to implement many operations of model checking more effectively. A model checker will check a single property of a single finite state system. The book examines various ways that this can be extended to handle—albeit partially—systems with infinite data domains, parameterized systems, and infinite state models. What are the prospects for model checking and verification in general A related technology is theorem proving: there are computer systems to build or at least to assist in building proofs that systems have particular properties. A proof is positive evidence that a system has a property, whereas a model checker produces no such evidence when it is successful. It is possible to construct proofs for (examples of) properties that are not amenable to decision procedures. Thus these two technologies complement each other, and currently one of the most fruitful lines of inquiry in logical verification is how to integrate model checking and theorem proving. This book can only promote this and other model checking research and development by providing such a thorough introduction to this burgeoning field.

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Browse Books

Sections

Cited By

Index Terms

Conditional model checking: a technique to pass information between verifiers

Model Checking CTL*[DC]

Modular Model Checking

Access critical reviews of Computing literature here

Save to Binder

Sections

Cited By

Save to Binder

Index Terms

Recommendations

Conditional model checking: a technique to pass information between verifiers

Model Checking CTL*[DC]

Modular Model Checking

Access critical reviews of Computing literature here