Beatrice Bérard, Michel Bidot, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Phillipe Schnoebelen, Pierre McKenzie.
Systems and Software Verification: model-checking techniques and tools.
Springer. 2001
Different techniques exist for the formal verification of critical systems (or part of them). This book is dedicated to model checking, one of the most widespread and efficient of these techniques.
Model checkers are used routinely by system designers to discover design errors
at an earlier stage in the project.
They are quickly becoming part of the standard toolkit,
especially in application domains such as:
• communication protocols
• VLSI circuits
• programmable logic controllers
• telephone services.
This book is the first text on model checking at a graduate/undergraduate level. It is divided into three parts. The first part is concerned with the fundamental notions (modelling with finite automata, synchronous product of automata, temporal logic, model-checking algorithms, symbolic model checking, timed systems). The second part focuses on the practical problem of writing correctness properties in temporal logic, and on different approaches to their verification. The third part reviews several model-checking tools.