This is a repository of system specifications written in Promela, the input language of the Spin model checker. Most of the models have been presented as case studies in international events (in particular in the international series of Spin workshops on software model checking). When possible the links point to the source code in the author's page. In the rest of the cases the sources are available on this site with the author's permisssion.
Most models are available in this file: promela-models.zip
Please do not hesitate to contact me to report new models, copyright violations, broken links or any other comment you might have.
BluespecTM Specifications
A chain of SystemC/TLM Modules
CORBA General Inter-Orb Protocol
- Authors: Moatz Kamel and Stefan Leue.
- Reference: Validation of a Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin (bibtex)
- Brief description: The general Inter-Orb Protocol (GIOP) is a key component of the OMG's Common Object Request Broker Architecture (CORBA) specification. It specifies a standard protocol that enables interoperability between ORB's from different vendors.
- Properties of the model:
- Scalable: yes (in the number of processes; the source contains several scaled models)
- Communication: basically by message passing (synchronous/asynchronous).
- Correctness Properties: satisfies various LTL properties. Absence of deadlocks and livelocks.
- State Space Size: about 2.8e+07 states.
- Some verification results (see reference for further results)
- Note: A deadlock can be seeded in the model by commenting out a timeout statement (see the source code for more explanation).
ITU-T T.122 and T.125
- Authors: Pedro Merino and J.M. Troya.
- Reference: Modeling and verification of the ITU-T multipoint communication service with SPIN (bibtex)
- Brief description: T.122 and T.125 are ITU-T recommendations for a multipoint communication service definition and protocol specification respectively.
- Properties of the models:
- Scalable: yes (in the number of processes).
- Communication: by shared variables and message passing (asynchronous).
- Correctness Properties: absence of deadlocks and livelocks.
- State Space Size: about 1e+03 states.
- Some verification results (see reference for further results)
- Note: includes the definition of predicates that can be used for constructing LTL formulas.
The Bounded Retransmission Protocol
- Authors: Pedro R. D'Argenio, Joost-Pieter Katoen, Theo C. Ruys and Jan Tretmans.
- Reference: The Bounded Retransmission Protocol must be on time! (bibtex)
- Brief description: The Bounded Retransmission Protocol is a protocol used in one of the Philips' products. It is based on the well known alternating bit protocol but allows for a bounded number of retransmissions of a chunk, i.e., part of a file, only. So, eventual delivery is not guaranteed and the protocol may abort the file transfer.
- Properties of the model:
- Scalable: no.
- Communication: by shared variables and message passing (synchronous/asynchronous).
- Correctness Properties: absence of deadlocks and livelocks. Satisfies an invariant.
- State Space Size: about 1e+05 states.
- Some verification results (see reference for further results)
PLC Control Schedule
- Authors: Ed Brinksma and Angelika Mader.
- Reference: Verification and Optimization of a PLC Control Schedule (bibtex)
- Brief description: The PLC Control Schedule is a model of a program for a Programmable Logic Controller of an experimental chemical plant.
- Properties of the model:
- Scalable: no.
- Communication: by shared variables.
- Correctness Properties: Absence of assertion violations. Presence of deadlocks.
- State Space Size: more than 7+06 states.
- Some verification results (see reference for further results)
Flight Guidance System
- Authors: Gerald Lüttgen and Victor Carreño.
- Reference: Analyzing Mode Confusion via Model Checking (bibtex)
- Brief description: FGS is a component of a flight guidance system used in avionics systems.
- Properties of the models:
- Scalable: no.
- Communication: by shared variables.
- Correctness Properties: absence of deadlocks and livelocks. Satisfies various assertions.
- State Space Size: about 2e+02 states.
- Some verification results (see reference for further results)
Steam Generator Control
- Author: Wenhui Zhang
- Reference: Model Checking Operator Procedures (bibtex)
- Brief description:
- Properties of the model:
- Scalable: no.
- Communication: by shared variables and message-passing (synchronous).
- Correctness Properties: absence of deadlocks and livelocks. Satisfies various LTL properties and violates others.
- State Space Size: about 3e+05 states.
- Some verification results (see reference for further results)
Space Craft Controller
- Authors: K. Havelund, M. Lowry and J. Penix.
- Reference: Formal Analysis of a Space Craft Controller using Spin (bibtex)
- Brief description: Model of a multi-threaded plan executing programming language. The language is one component of NASA's New Millennium Remote Agent, an artificial intelligence based spacecraft control system architecture.
Group Address Registration Protocol
- Authors: Tadashi Nakatani.
- Reference: Verification of Group Address Registration Protocol using PROMELA and SPIN
- Brief description: The Group Address Registration Protocol (GARP) is a datalink-level protocol for dynamically joining and leaving multicast groups on a bridged LAN.
- Properties of the models:
- Scalable: yes (in the number of processes).
- Communication: by message-passing (synchronous and asynchronous).
- Correctness Properties: absence of deadlocks and livelocks. Satisfies various LTL properties.
- State Space Size: about 6.4e+06 states.
- Some verification results (see reference for further results)
- Notes: If a full queue blocks new messages, then the model deadlocks. The "correct" verification must be done by setting that a full queue loses new messages.
X.509 Authentication Protocol
- Authors: Audun Josang.
- Reference: Security Protocol Verification using SPIN (bibtex)
- Brief description: X.509 is a CITT recommendation for an authentication protocol. It gives details of a method of allowing a user agent to send a password to a system agent in a safe manner that is not vulnerable to interception or replay.
- Properties of the model:
- Scalable: no.
- Communication: by message-passing (asynchronous) and shared variables.
- Correctness Properties: absence of deadlocks and livelocks. Violation of an assertion.
- State Space Size: about 7e+03 states.
- Some verification results (see reference for further results)
Data Base Manager
- Authors: Dragan Bosnacki, Dennis Dams and Leszek Holenderski
- Reference: Symmetric Spin (bibtex)
- Brief description: Promela Model after the description of a The Database Manager Protocol by A. Valmari.
- Properties of the model:
- Scalable: yes (in the number of processes).
- Communication: by shared variables.
- Correctness Properties: absence of deadlocks, livelocks and violations of assertions.
- State Space Size: about 5e+03 states.
- Some verification results (see reference for further results)
Relay Circuits
- Author: Peter van Eijk.
- Reference: Verifying Relay Circuits using State Machines (bibtex)
- Brief description: Promela Models of various electro-mechanical relay circuits.
- Properties of the models:
- Scalable: no.
- Communication: by shared variables.
- Correctness Properties: absence of deadlocks and livelocks. One of the models violate an assertion.
- State Space Size: about 2.67e+04 states (the largest model).
- Some verification results (see reference for further results)
- Notes: several models.
Cash Machine System
- Authors: Jeffery Tang and Wei Zhou.
- Reference: Cash Point with Promela/Spin
- Brief description: Promela Model of a software controller for a cash machine system that involves multiple cash tills and users.
- Properties of the models:
- Scalable: yes (in the number of processes).
- Communication: by message-passing (asynchronous) and shared variables.
Taylor's I-Protocol
- Authors: Yifei Dong, Xiaoqun Du, Y.S. Ramakrishna, C.R. Ramakrishnan, I.V. Ramakrishnan, Scott A. Smolka, Oleg Sokolsky, Eugene W. Stark, and David S. Warren.
- Reference: Fighting Livelock in the i-Protocol: A Comparative Study of Verification Tools
- Brief description: The i-protocol is an optimized sliding-window protocol for GNU UUCP. It is an asynchronous, low-level software system equipped with a number of optimizations aimed at minimizing control-message and retransmission overhead. It lacks the regular structure that is often present in hardware designs.
- Properties of the model:
- Scalable: no.
- Communication: by message passing (asynchronous).
- Correctness Properties: presence of deadlocks and livelocks.
- State Space Size: about 9.19e+05 states.
- Some verification results (see reference for further results)
Needham-Schroeder Public Key Protocol
- Authors: Paolo Maggi and Riccardo Sisto.
- Reference: Using SPIN to Verify Security Properties of Cryptographic Protocols (bibtex)
- Brief description: The Needham-Schroeder Public Key Protocol is a well known authentication protocol that aims to establish mutual authentication between an initiator and a responder. The model implements an instance of the protocol including an intruder.
- Properties of the models:
- Scalable: no.
- Communication: message passing (asynchronous).
- Correctness Properties: some models satisfy and other violate an LTL property.
- State Space Size: about 7e+03 states.
- Some verification results
Harmony Multiprocessor Real-Time Kernel
- Authors: Thierry Cattel.
- Reference: Modelling and verification of a multiprocessor realtime OS kernel
- Brief description: Harmony is a porbale real-time multitasking multiprocessor operating system being developed at the NRC since the early 80's. Basically, it is an operating system based on a micro-kernel and system servers. The features of the kernel are interryp management, task scheduling, intertask communication, dynamic task managemente, memory managemend and I/O.
- Properties of the model:
- Scalable: yes.
- Communication: by shared variables and message passing (asynchronous).
- Correctness Properties: Presence of deadlocks and violation of assertions.
- State Space Size: about 2e+03 states
- Some verification results (see reference for further results)
Steam Boiler
A Bus Arbiter
- Authors: Samuel Devulder.
- Reference: A comparison of LPV with other validation methods
- Brief description:The basic informal specification is the following: several identical users can ask the access to a bus. The system must give the access to at most one user, and exactly one if there is actually a pending request (ie. there must be no delay to grant the access to the bus if only one user asks for it).
- Properties of the model:
- Scalable: yes.
- Communication: by shared variables.
- Correctness Properties: absence of deadlocks, and satisfaction of an invariant.
- State Space Size: about 1.29e+02 states
- Some verification results (see reference for further results)
The Conference Protocol
- Authors: Theo C. Ruys, Rene G. de Vries
- Reference: Conference Protocol Case Study
- Brief description:The conference protocol provides a multicast service, resembling a `chatbox', to users participating in a conference. A conference is a group of users that can exchange messages to all conference partners in that conference. So, every user can send messages to, or receive messages from, all its conference partners.
- Properties of the model:
- Scalable: no.
- Communication: by message passing (synchronous and asynchronous).
Fluke's IPC Mechanism
- Authors: Patrick Tulmann, John McCorquodale, Ajay Chitturi, Godmar Back, and Jeff Turner.
- Reference: Verifying Fluke IPC
- Brief description: -
- Properties of the model:
Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking
Leader election algorithms for anonymous rings
Itai Rodeh leader election algorithms
Cardiac Pacemaker Model
Internet Key Exchange Protocol Version 2 (IKEv2)
- Authors: Tristan Ninet, Axel Legay, Romaric Maillard, Louis-Marie Traonouez and Olivier Zendra.
- Reference: Formal verification of the Internet Key Exchange (IKEv2) security protocol, Sections 3.2 and 3.3
- Brief description: We analyze the IKEv2 protocol specification using Spin. To do so, we extend and improve an existing modeling method with a more scalable adversary model, a model for common cryptographic primitives and Lowe's authentication properties.
- Source Code: here.
ALICE Data Point Processing Framework
ALICE Data Point Service
NOTES
- The size of the state space given has been calculated by performing an exhaustive exploration of the model using partial order reduction. In the case of scalable models a medium-size configuration has been explored. The same can be said for the verification results.
- A lot of models can be found in the Spin distribution: X.21, ackerman's protocol, alternating bit protocol, barlett's protocol, cambridge, cribe of erathostenes, go-back-n retransmission protocol, leader election protocol, lynch's protocol, a model of cell-phone handoff strategy in a mobile network, optical telegraph protocol, pathfinder scheduling algorithm, peterson's algorithm, a model of a petri net, pftp, snoopy protocol, sleep-wake up, sort.
(for contributions, problems, etc. do not hesitate to contact me)