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
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.
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
The sources of the
extension are written in ANSI standard C and can be downloaded from here or obtained from Dragan Bosnacki (email@example.com). The extension is portable to the same platforms as the standard
distribution - Unix systems and Windows 95/Windows NT PC's.
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
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: firstname.lastname@example.org.