zbMATH — the first resource for mathematics

Systems and software verification. Model-checking techniques and tools. (English) Zbl 1002.68029
Berlin: Springer. xii, 196 p. (2001).
In significant hardware designs or embedded software projects the system complexity, and hence the likely number of design errors, grows exponentially with the number of interacting system components. Traditional debugging and validation techniques are inadequate for detecting errors. Better suited are model-checking-based techniques. Model checking was invented more than twenty years ago but it is still developing and has more recently been introduced in many application fields.
The book is an intelligible introduction to model checking. It is divided into three parts presenting fundamentals, including modelling with finite automata, synchronized product automata, introduction to temporal logics (CTL*, CTL, PLTL), algorithms of model checking and symbolic model checking, and an introduction to timed automata together with TCTL; specification and proof of selected properties, widely used in practice (reachability of states, safety, liveness, fairness, deadlock-freeness); an introduction to six tools, freely available in the academic world, considered from a user’s point of view.
The book can be used as an introductory textbook at an undergraduate or graduate level even though it has not the form of a typical modern textbook. More practically oriented readers will find a lot of examples illustrating theoretical considerations and hints how to catch special practical problems as, e.g., the state explosion problem.

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68-01 Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science