The model checker SPIN
- 1 May 1997
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. 23 (5) , 279-295
- https://doi.org/10.1109/32.588521
Abstract
SPIN is an efficient verification system for models of distributed software systems. It has been used to detect design errors in applications ranging from high-level descriptions of distributed algorithms to detailed code for controlling telephone exchanges. This paper gives an overview of the design and structure of the verifier, reviews its theoretical foundation, and gives an overview of significant practical applications.Keywords
This publication has 32 references indexed in Scilit:
- Symbolic protocol verification with queue BDDsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formalization and validation of the Radio Link Protocol (RLP1)Computer Networks and ISDN Systems, 1997
- Using partial-order methods in the formal validation of industrial concurrent programsIEEE Transactions on Software Engineering, 1996
- Evaluating deadlock detection methods for concurrent softwareIEEE Transactions on Software Engineering, 1996
- Reactive EFSMs — Reactive Promela/RSPINPublished by Springer Nature ,1996
- Formal verification of a partial-order reduction technique for model checkingPublished by Springer Nature ,1996
- Formal Validation of a High Performance Error Control Protocol Using SPINSoftware: Practice and Experience, 1996
- Symbolic Model CheckingPublished by Springer Nature ,1993
- The temporal logic of programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1977
- Theories of automata on ω-tapes: A simplified approachJournal of Computer and System Sciences, 1974