Principles of the Spin Model Checker

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...

Full description

Main Author: Ben-Ari, Mordechai
Corporate Author: SpringerLink (Online service)
Format: eBook
Published: London Springer London 2008, 2008
Edition:1st ed. 2008
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
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