Principles of the Spin Model Checker

• Main Author: Ben-Ari, Mordechai (Author)
• Corporate Author: SpringerLink (Online service)
• Format: Electronic eBook
• Language: English
• Published: London : Springer London, 2008.
• Subjects: Computer science.; Software engineering.; Computer programming.; Programming languages (Electronic computers).; Operating systems (Computers).; Computers.; Computer logic.; Computer Science.; Software Engineering/Programming and Operating Systems.; Programming Techniques.; Programming Languages, Compilers, Interpreters.; Operating Systems.; Theory of Computation.; Logics and Meanings of Programs.

The Spin model checker is a widely used professional software tool for specifying and verifying concurrent and distributed systems. Models, written in a simple language called Promela, can be simulated randomly or interactively. Spin can generate efficient verifiers that search for a counterexample...

Table of Contents:

• Sequential Programming in Promela
• Verification of Sequential Programs
• Concurrency
• Synchronization
• Verification with Temporal Logic
• Data and Program Structures
• Channels
• Nondeterminism
• Advanced Topics in Promela
• Advanced Topics in Spin
• Case Studies.