B. Berard, M. Bidoit, A. Finkel

Systems and Software Verification

Model-Checking Techniques and Tools
Übersetzung:McKenzie, P.

• Broschiertes Buch

Produktbeschreibung

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.

Produktdetails

• Verlag: Springer / Springer Berlin Heidelberg / Springer, Berlin
• Artikelnr. des Verlages: 978-3-642-07478-3
• Softcover reprint of hardcover 1st ed. 2001
• Seitenzahl: 208
• Erscheinungstermin: 15. Dezember 2010
• Englisch
• Abmessung: 235mm x 155mm x 12mm
• Gewicht: 324g
• ISBN-13: 9783642074783
• ISBN-10: 3642074782
• Artikelnr.: 32079019

Inhaltsangabe

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.