The model checker SPIN
IEEE Transactions on Software EngineeringPublished 1 May 1997
Gerard J. Holzmann
Citations3,736
SJR quartileQ1
SJR score1.45
SNIP2.43
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
An overview of the design and structure of the verifier, its theoretical foundation, and an overview of significant practical applications are given.
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. The 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
Computer Science
SIAM Journal on ComputingDepth-First Search and Linear Graph Algorithms
6,021 Citations1972Robert E. Tarjan
The value of depth-first search or “backtracking” as a technique for solving problems is illustrated by two examples of an improved version of an algorithm for finding the strongly connected components of a directed graph.
The temporal logic of programs
5,586 Citations1977Amir Pnueli
A unified approach to program verification is suggested, which applies to both sequential and parallel programs, and the main proof method is that of temporal reasoning in which the time dependence of events is the basic concept.
Lecture notes in computer scienceSymbolic model checking
2,843 Citations1996Emma L. Clarke, K. McMillan +2 more
Using symbolic model checking techniques it is possible to verify industrial-size finite state systems and models with more than 10120 states have been verified using special techniques.
Information and ComputationSymbolic model checking: 1020 States and beyond
2,674 Citations1992Jerry R. Burch, E. M. Clarke +3 more
It is shown how the novel mu-calculus model checking algorithm can be used to derive efficient decision procedures for CTL model checking, satisfiability of linear-time temporal logic formulas, strong and weak observational equivalence of finite transition systems, and language containment of finite omega -automata.
Lecture notes in computer scienceDesign and synthesis of synchronization skeletons using branching time temporal logic
2,137 Citations2005Edmund M. Clarke, E. Allen Emerson
It is shown that it is possible to automatically synthesize the synchronization skeleton of a concurrent program from a Temporal Logic specification and it is believed that this approach may in the long run turn out to be quite practical.
Design and validation of computer protocols
1,695 Citations1991Gerard J. Holzmann
Part 1 Basic: introduction protocol structure error control flow control and design tools: a protocol simulator a protocol validator using the validator.
Symbolic Model Checking
1,645 Citations1993Kenneth L. McMillan
The symbolic model checking technique revealed subtle errors in this protocol, resulting from complex execution sequences that would occur with very low probability in random simulation runs, and an alternative method is developed for avoiding the state explosion in the case of asynchronous control circuits.
Lecture notes in computer scienceSpecification and verification of concurrent systems in CESAR
1,277 Citations1982J. P. Queille, Joseph Sifakis
By an example, the alternating bit protocol, the use of CESAR, an interactive system for aiding the design of distributed applications, is illustrated.
Open Repository and Bibliography (University of Liège)An Automata-Theoretic Approach to Automatic Program Verification
1,254 Citations1986Moshe Y. Vardi, Pierre Wolper
Elsevier eBooksAutomata on Infinite Objects
947 Citations1990Wolfgang Thomas
This chapter discusses the formulation of two interesting generalizations of Rabin's Tree Theorem and presents some remarks on the undecidable extensions of the monadic theory of the binary tree.
Information and ComputationReasoning about Infinite Computations
794 Citations1994Moshe Y. Vardi, Pierre Wolper
This work investigates extensions of temporal logic by connectives defined by finite automata on infinite words and shows that they do not increase the expressive power of the logic or the complexity of the decision problem.
Computers & Mathematics with ApplicationsComputer-aided verification of coordinating processes: The automata-theoretic approach
793 Citations1995
Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem
771 Citations1996Patrice Godefroid, Jan Van Leeuwen +3 more
IFIP advances in information and communication technologySimple On-the-fly Automatic Verification of Linear Temporal Logic
695 Citations1996Rob Gerth, Doron Peled +2 more
A tableau-based algorithm for obtaining an automaton from a temporal logic formula that can be constructed simultaneously with, and guided by, the generation of the model, and which can be used in model checking in an “on-the-fly” fashion.
Lecture notes in computer scienceAn automata-theoretic approach to linear temporal logic
654 Citations1996Moshe Y. Vardi
The automata-theoretic approach to linear temporal logic uses the theory of automata as a unifying paradigm for program specification, verification, and synthesis and considers the relationships between programs and their specifications as relationships between languages.
Lecture notes in computer sciencePartial-Order Methods for the Verification of Concurrent Systems
618 Citations1996
Using partial orders to tackle state explosion and persistent sets for verification of safety properties and model checking are used.
Formal Methods in System DesignMemory-efficient algorithms for the verification of temporal properties
498 Citations1992C. Courcoubetis, M. Vardi +2 more
Algorithms are presented that solve the emptiness problem without explicitly constructing the strongly connected components of the graph representing the product automaton by allowing the algorithms to err with some probability.
Princeton University Press eBooksComputer-Aided Verification of Coordinating Processes
441 Citations1995Robert P. Kurshan
Theories of L-automaton/L-process, L-matrix, and String Acceptors are compared to Boolean Algebra, which describes the construction of language-based Algebra.
Lecture notes in computer scienceCombining partial order reductions with on-the-fly model-checking
260 Citations1994Doron Peled
Expressing interesting properties of programs in propositional temporal logic
255 Citations1986Pierre Wolper
It is shown that the class of properties of programs expressible in propositional temporal logic can be substantially extended if the authors assume the programs to be data-independent.
Workshops in computingSpecification and Verification of Concurrent Systems
232 Citations1990Charles Rattray
This book discusses the Interplay of Theory and Practice in a Parallel Object-Oriented Language, and a Functional Programming Approach to the Specification and Verification of Concurrent Systems.
IFIP advances in information and communication technologyAn Improvement in Formal Verification
230 Citations1995Gerard J. Holzmann, Doron Peled
This paper proposes a new reduction method that solves some of the problems of redundancy caused by the many possible interleavings of inde- pendent actions in a concurrent system.
IEEE Transactions on Software EngineeringEvaluating deadlock detection methods for concurrent software
230 Citations1996James C. Corbett
An evaluation of three techniques for combating the state explosion problem in deadlock detection: reachability searching with a partial-order state-space reduction, symbolic model checking and inequality-necessary conditions.
Journal of Computer and System SciencesTheories of automata on ω-tapes: A simplified approach
210 Citations1974Yaacov Choueka
Using a combinatorial lemma on regular sets, and a technique of attaching a control unit to a parallel battery of finite automata, a simple and transparent development of McNaughton's theory of automata on @w-tapes is given.
Journal of AlgorithmsAn O(n log n) unidirectional distributed algorithm for extrema finding in a circle
203 Citations1982Danny Dolev, Maria Klawe +1 more
Algorithms, which given a circular arrangement of n uniquely numbered processes, determine the maximum number in a distributive manner, disprove Hirschberg and Sinclair's conjecture that O ( n 2 ) is a lower bound on the number of messages passed in undirectional algorithms.
DIMACS series in discrete mathematics and theoretical computer scienceOn nested depth first search
186 Citations1997Gerard J. Holzmann, Doron Peled +1 more
It is shown that the algorithm for solving the model checking problem with a nested depth-first search can interfere with algorithms that support partial order reduction, and a revised version of the algorithm is introduced that guarantees compatibility.
IBM Journal of Research and DevelopmentGeneral Technique for Communications Protocol Validation
133 Citations1978Colin H. West
The validation exhaustively exercises the interaction domain of a system and identifies all occurrences of a number of well-defined error conditions that can detect when individual processes have no predefined response to incoming messages.
Software Practice and ExperienceAn improved protocol reachability analysis technique
131 Citations1988Gerard J. Holzmann
An automated analysis of all reachable states in a distributed system can be used to trace obscure logical errors that would be very hard to find manually.
CERN Document Server (European Organization for Nuclear Research)Distributed Algorithms and Protocols
127 Citations1988Michel Raynal
This book attempts to provide a clear, practical and up-to-date guide to distributed algoriths and protocols in the area of control and describes the algorithms to solve it.
Computer Networks and ISDN SystemsDesign and validation of protocols: a tutorial
125 Citations1993Gerard J. Holzmann
In this tuturial a state-of-the-art tool called SPIN and the specification language PROMELA are introduced and it is shown how the language and the tool can be used to design reliable protocols.
State Compression in SPIN: Recursive Indexing and Compression Training Runs
96 Citations2002Gerard J. Holzmann
The verification algorithm of SPIN is based on an explicit enumeration of a subset of the reachable state-space of a system that is obtained through the formalization of a correctness requirement as an ω-automaton.
Elsevier eBooksCoverage Preserving Reduction Strategies for Reachability Analysis
92 Citations1992Gerard J. Holzmann, Patrice Godefroid +1 more
Three new reduction strategies for conventional reachability analysis, as used in automated protocol validation algorithms, are shown to have a potential for substantially improving the performance of a conventional search.
Lecture notes in computer scienceExtending promela and spin for real time
77 Citations1996Stavros Tripakis, Costas Courcoubetis
This work extends the syntax and semantics of the higher level specification language Promela to include constructs and statements based on the model of timed Buchi automata, and implements these extensions on top of the verification tool Spin.
IEEE Transactions on Software EngineeringAutomated Protocol Validation in Argos: Assertion Proving and Scatter Searching
77 Citations1987Gerard J. Holzmann
A model in Argos is constructed consisting of a control flow specification and a formal description of the correctness requirements that can be compiled into a minimized lower level description based on a formal model of communicating finite state machines.
On the Verification of Temporal Properties
60 Citations1993Patrice Godefroid, Gerard J. Holzmann
The new algorithm is simpler than the traditional algorithm of Tarjan to check for maximal strongly connected components in a directed graph which is the classical algo- rithm used for modelchecking, but requires less memory.
IFIP advances in information and communication technologyAn analysis of bitstate hashing
57 Citations1996Gerard J. Holzmann
AT&T Technical JournalAlgorithms for Automated Protocol Verification
56 Citations1990Gerard J. Holzmann
The algorithm derived in this manner works in a fixed-size memory arena (it will never run out of memory), it is up to 2 orders of magnitude faster than the previous methods, and it has superior coverage of the state space when analyzing large protocol systems.
AT&T Technical JournalTracing Protocols
55 Citations1985Gerard J. Holzmann
The paper addresses the problem of finding errors in data communication protocols of which the size precludes analysis by traditional means and describes the protocol tracing method, which allows one to locate design errors in protocols relatively quickly by probing a partial state space.
Lecture notes in computer scienceFormal verification of a partial-order reduction technique for model checking
41 Citations1996C.-T. Chou, Doron Peled
Lecture notes in computer scienceModel Checking Safety Critical Software with SPIN: an Application to a Railway Interlocking System
35 Citations1998Alessandro Cimatti, Fausto Giunchiglia +4 more
This paper describes how a formal model of the Safety Logic has been develped in the language of the spin model checker and discusses how the automated verification of several significant process configurations was carried out without incurring into the state explosion problem.
ComputerCodesign of communication protocols
33 Citations1993Alan Wenban, John O’Leary +1 more
A codesign process using Promela, a concurrent programming language, is under development and as an example, the method is applied to a simple communication system using the alternating bit protocol.
Defense Technical Information Center (DTIC)Verifying SCR Requirements Specifications Using State Exploration
32 Citations1997Ramesh Bharadwaj, Constance Heitmeyer
How SCR specifications can be translated into an imperative programming notation is described and how to limit state explosion by verifying abstractions of the original requirements specification is described.
IEEE SoftwareProtocol design: redefining the state of the art
28 Citations1992Gerard J. Holzmann
The application of formal methods to high-level protocol design is addressed and the framework for proving logical correctness in protocol engineering is discussed.
DIMACS series in discrete mathematics and theoretical computer scienceThe application of PROMELA and SPIN in the BOS project
27 Citations1997Pim Kars
After a short introduction to the BOS project, the why, what and how of the use of formal methods in the project are discussed, some recent experience using Promela/Spin is discussed and re ections on the pragmatics of validation are discussed.
Elsevier eBooksFormal Methods at AT&T - An Industrial Usage Report
26 Citations1992John A. Chaves
The NewCoRe 1 project is developing an approach for the systematic application of formal methods for design and verification specifically for use in the context of large scale software development.
Journal of Thoracic DiseaseA language-based approach to protocol construction
23 Citations1998Anindya Basu
HRV is a common etiology in CAP among China adults, especially in severe CAP, and highly qualified multiplex PCR techniques with invasive sampling are needed to increase the detection rate.
IEEE Transactions on Software EngineeringUsing partial-order methods in the formal validation of industrial concurrent programs
22 Citations1996Patrice Godefroid, Doron Peled +1 more
Lecture notes in computer scienceModel checking in practice: An analysis of the ACCESS.bus™ protocol using SPIN
21 Citations1996Bernard Boigelot, Patrice Godefroid
This paper presents a case study of the use of model checking for analyzing an industrial protocol, the ACCESS.bus™ protocol, and reveals subtle flaws in the design of the protocol.
Symbolic protocol verification with queue BDDs
21 Citations2002Patrice Godefroid, David E. Long
This work introduces Queue BDDs (QBDDs), which include all the power of B DDs while also providing an efficient representation of queue contents, and Experimental results show that QBDDs are well-suited for the verification of communication protocols.
Formal methods: a practical tool for OS implementors
20 Citations2002Patrick Tullmann, Joseph A. Turner +4 more
This paper applied formal methods to verify properties of the implementation of the Fluke microkernel's IPC subsystem, a major component of the kernel, and presents the results as a starting point for a more comprehensive inclusion of formal methods in practical OS development.
Computer CommunicationsDesigning bug-free protocols with SPIN
10 Citations1997Gerard J. Holzmann
This paper outlines the use of the SPIN tool to address protocol design problems and considers the verification of a published protocol for implementing synchronous rendezvous operations in a distributed system.
Process Sleep and Wakeup on a Shared-memory Multiprocessor
9 Citations1991Robert N. Pike, Dave Presotto +2 more
The code for sleep and wakeup primitives is presented, exercised by years of active use and by a verification system, to synchronise processes on a symmetric shared-memory multiprocessor system.
IFIP advances in information and communication technologyModelling and Verification of a Multiprocessor Realtime OS Kernel
9 Citations1995Thierry Cattel
It is shown that it is possible to detect more than deadlocks when using formal methods for the study of a real medium-sized operating system that encompasses complex internal management.
Pan - A Protocol Specification Analyzer
8 Citations2002Gerard J. Holzmann
Pan is a program that can analyze the consistency of protocol specification for up to ten interacting processes using a special algebra for an extended type of regular expressions, named protocol expressions.
IEEE/ACM Transactions on NetworkingA unified approach to fault-tolerance in communication protocols based on recovery procedures
7 Citations1996Anjali Agarwal, J. William Atwood
The recovery procedure provides a legal protocol state, which is the global state before reaching any illegal state and before the effects of the error make other states illegal, and is compared with the existing approaches of handing the errors.
Explicit-enumeration based verification made memory-efficient
7 Citations2002Ratan Nalumasu, G. Gopalakrishnan
New techniques for reducing the memory requirements of an on-the-fly model checking tool that employs explicit enumeration are investigated: exploiting symmetries in the model, and exploiting sequential regions in themodel.
IFIP advances in information and communication technologyUsing Concurrency and Formal Methods for the Design of Safe Process Control
6 Citations1996Thierry Cattel
This application shows that formal methods are quite appropriate for developing control process problem from scratch and with requirements to be checked in mind.
Computer Networks and ISDN SystemsFormalization and validation of the Radio Link Protocol (RLP1)
5 Citations1997M.J. Ferguson
The formalization and validation of the Radio Link Protocol (RLP1) and the effect of the validation on its standardization are described and it is argued that a suite of accepted formal notations is necessary to formalize the many different parts of a protocol standard.
Software Practice and ExperienceFormal Validation of a High Performance Error Control Protocol Using SPIN
4 Citations1996Toong Shoon Chan, Ian Gorton
The specification and validation of a high performance error control protocol using the PROMELA language has demonstrated the advantage of employing formal validation methods in designing distributed systems.
Lecture notes in computer scienceReactive EFSMs — Reactive Promela/RSPIN
4 Citations1996Elie Najm, Frank Olsen
The ideas presented are discussed first in a formal setting then they are discussed their implementation in Reactive Promela and RSPIN concrete syntax and tool.
SPIN as a Hardware Design Tool
3 Citations1995Budi Rahardjo
This paper presents the application of SPIN to verify a hardware design modelled in PROMELA and verified with SPIN, showing the presense of hazard.
National Research Council Canada (Government of Canada)Verifying Semantic Relations in SPIN
3 Citations2002Hakan Erdogmus
The Spine system extends Spin with `limited' semantic relation checking capability implemented in terms of a new option, -e, whose usage is given below:.