UID:
almahu_9948621311002882
Format:
XII, 190 p.
,
online resource.
Edition:
1st ed. 2001.
ISBN:
9783662045589
Content:
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.
Note:
1. Automata -- 2. Temporal Logic -- 3. Model Checking -- 4. Symbolic Model Checking -- 5. Timed Automata -- 6. Reachability Properties -- 7. Safety Properties -- 8. Liveness Properties -- 9. Deadlock-freeness -- 10. Fairness Properties -- 11. Abstraction Methods -- 12. SMV - Symbolic Model Checking -- 13. SPIN - Communicating Automata -- 14. DESIGN/CPN - Coloured Petri Nets -- 15. UPPAAL - Timed Systems -- 16. KRONOS - Model Checking of Real-time Systems -- 17. HYTECH - Linear Hybrid Systems -- Main Bibliography.
In:
Springer Nature eBook
Additional Edition:
Printed edition: ISBN 9783642074783
Additional Edition:
Printed edition: ISBN 9783540415237
Additional Edition:
Printed edition: ISBN 9783662045596
Language:
English
DOI:
10.1007/978-3-662-04558-9
URL:
https://doi.org/10.1007/978-3-662-04558-9
Bookmarklink