Real-Time Spin (RT-Spin) extends the verification tool Spin with quantitative dense time features. This means that properties such as ``between event a and event b at least 5 time units should pass'' can be expressed (quantitative time), independently of a specific time unit (dense time).
The input language of RT-Spin is Real-Time Promela. Like Spin,
RT-Spin works as a code generator: it takes as input a specification written
in RT-Promela, and generates a set of C files, to be compiled into an analyser.
In the case of RT-Spin, the compiled C files must also be linked with some
object files which implement the symbolic operations on DBMs (matrices
representing real-time information). The analyser is then executed with
various options, to verify the correctness of the specification.
The real-time extensions of Promela, as well as some of the features of RT-Spin, are described in the paper:
RT-Spin is free for non-military purposes. rtspin-distr.tar.gz is a gzipped tar-file containing the sources of the code generator, as well as the object files for Sun4 and Sun5 (Solaris) systems. (Make sure that the "arch" command of your system returns the correct architecture value, namely, sun4 or sun5. This is not always the case, eg, for Sun4 systems ported to Solaris, without caring to update the variable read by "arch". In case of an inconsistency, set "manually" the makefile macro "ARCH" to the proper value.) rtspin-linux.tar.gz is a gzipped tar-file containing the sources of the code generator, as well as the object files for Linux systems.
To install the tool, follow the instructions in the README file. You should only need to complete the lines:
Then, you should create rtspin by issuing "make spin". Run rtspin on the example:
and create the analyser by issuing "make ttt". You can run it with various options, see "-?". In particular, helpful options for real-time programs are:
Back to home page of Stavros Tripakis