Systems and Software Verification : Model-Checking Techniques and Tools

"Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available."--Publisher's website Front Matter....Pages I-XII Front Matter....Pages 1-3 Automata....Pages 5-26 Temporal Logic....Pages 27-38 Model Checking....Pages 39-46 Symbolic Model Checking....Pages 47-58 Timed Automata....Pages 59-72 Front Matter....Pages 75-78 Reachability Properties....Pages 79-81 Safety Properties....Pages 83-89 Liveness Properties....Pages 91-98 Deadlock-freeness....Pages 99-101 Fairness Properties....Pages 103-107 Abstraction Methods....Pages 109-123 Front Matter....Pages 127-130 SMV — Symbolic Model Checking....Pages 131-138 SPIN — Communicating Automata....Pages 139-144 DESIGN/CPN — Coloured Petri Nets....Pages 145-151 UPPAAL — Timed Systems....Pages 153-159 KRONOS — Model Checking of Real-time Systems....Pages 161-168 HYTECH — Linear Hybrid Systems....Pages 169-177 Back Matter....Pages 179-190 "Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available."--Résumé de l'éditeur

Model checking is a powerful approach for the formal verification of software. It automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. Here, the author provides a well written and basic introduction to the new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available.