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
Check out the user and developer manual: TopSPIN_2.2_manual.pdf.
If you use TopSPIN in your work and wish to cite it, please refer to our AMAST 2006 tool paper.
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.
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.