TopSPIN

Automatic Symmetry Reduction for the SPIN Model Checker


Alastair F. Donaldson and Alice Miller
Email: alastairZZZ.donaldson@imperial.ac.uk [remove ZZZ]

Overview

TopSPIN is an automatic symmetry reduction tool for the SPIN model checker. TopSPIN is applied to a Promela specification, and, provided that the specification adheres to some restrictions (detailed in the user manual), uses computational group theory to automatically determine a group of component symmetries associated with the specification. The tool automatically modifies the model checking algorithm employed by SPIN to exploit these symmetries during verification. This can result in significantly reduced memory consumption, and in many cases also in faster verification time.

TopSPIN was designed at the Department of Computing Science, University of Glasgow, by Alastair Donaldson and Alice Miller.

Downloading and Using TopSPIN

Download the latest TopSPIN release

Documentation

Check out the user and developer manual: TopSPIN_2.2_manual.pdf.

Examples

A zip of example Promela specifications for use with TopSPIN is available, which includes the specifications described in the AMAST and FM papers, and in my Ph.D. thesis.

Citing TopSPIN

If you use TopSPIN in your work and wish to cite it, please refer to our AMAST 2006 tool paper.

Feedback

The user manual contains information about common problems people have encountered when using TopSPIN. If this information is not sufficient, please send error reports on TopSPIN to Alastair Donaldson (email address above). Please also send other feedback on the tool to this address.

Old Version

The version of TopSPIN used in the AMAST and FM papers is still available for download: TopSPIN-1.2.zip, together with a short user manual with installation instructions for that version. However, this version of TopSPIN is not supported.