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 desc...
| Main Author: | |
|---|---|
| Corporate Author: | |
| Other Authors: | , , , , , , |
| Format: | eBook |
| Language: | English |
| Published: |
Berlin, Heidelberg :
Springer Berlin Heidelberg,
2001.
|
| Subjects: | |
| Online Access: | Connect to the full text of this electronic book |
| Summary: | 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. |
|---|---|
| Item Description: | Electronic resource. |
| Physical Description: | 1 online resource (xii, 190 pages 67 illustrations) |
| ISBN: | 9783662045589 (electronic bk.) 3662045583 (electronic bk.) |