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:

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

ITU-T T.122 and T.125

The Bounded Retransmission Protocol

PLC Control Schedule

Flight Guidance System

Steam Generator Control

Space Craft Controller

Group Address Registration Protocol

X.509 Authentication Protocol

Data Base Manager

Relay Circuits

Cash Machine System

Taylor's I-Protocol

Needham-Schroeder Public Key Protocol

Harmony Multiprocessor Real-Time Kernel

Steam Boiler

A Bus Arbiter

The Conference Protocol

Fluke's IPC Mechanism

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


(for contributions, problems, etc. do not hesitate to contact me)