Discrete-time Promela and Spin

Spin is a software package for the specification and verification of concurrent systems, created and developed by Gerard Holzmann at Bell Labs. The formal models of the systems that are simulated or verified are written in Promela, Spin's input language. For complete information about the standard distribution, downloading of executables and sources, installation, license etc., please visit Spin's home page or have a look at

G. J. Holzmann, "Design and Validation of Communication Protocols", Prentice Hall, 1991

DTSpin is an extension of Spin with discrete time, and it is intended for verification of concurrent systems that depend on timing parameters. The extension is completely compatible with the standard untimed version of the Spin validator, except for the timeout statement, which has different semantics and its usage is not allowed (and not necessary) any more in the discrete-time models. More information about DTSpin and its input language DTPromela can be found here.

Download

If you want to try DTSpin you might need the following files:

DTSpinLinux.bin , the executable version of DTSpin for Linux

dtime.h - a header file with the definition of discrete-time macros that should be included in every Discrete-time Promela model,

and some models of communication protocols written in Discrete-time Promela

PAR- Parallel Acknowledgment with Retransmission Protocol
Fischer - Fischer's mutual exclusion protocol
BRP - Bounded Retransmission protocol

The sources of the extension are written in ANSI standard C and can be downloaded from here or obtained from Dragan Bosnacki (dragan@win.tue.nl). The extension is portable to the same platforms as the standard distribution - Unix systems and Windows 95/Windows NT PC's.

Usage

The usage of DTSpin is the same as for the standard Spin. To try some of the examples, say Fischer, assuming that the executable is renamed into dtspin, you should first generate the verifier - a set of C files (main file being called pan.c), with

dtspin -a Fischer

Then the analyser should be compiled into an executable, for instance with,

gcc -DSAFETY -DNOFAIR -o pan pan.c

The last phase is to execute the verifier by typing

pan

Also DTSpin can be used from xspin (version 3.3.10) in the same way as the standard Spin.

If you have any problems with the tool, or want some more information, please write to Dragan Bosnacki: dragan@win.tue.nl.