Natalia Ioustinova , Specification and Analysis of Embedded Systems

Verifying open Discrete-Time Promela models

Discrete-time Promela and Spin

The first version of the model checker SPIN was introduced in 1991 by

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

DTSpin is a discrete time extension of SPIN developed by Dragan Bosnacki 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. For complete information about the distribution, downloading of executables and sources, installation etc., please visit DTSpin home page

Verifying open Discrete-Time Promela models

Model checking would answer all finite-state verification problems, if it were not for the notorious state-space explosion problem. A problem of practical importance, which attracted less attention, is to close open systems. Standard model checkers cannot handle open systems directly and closing is commonly done by adding an environment process, which in the simplest case behaves chaotically. However, for model checking, the way of closing should be well-considered to alleviate the state-space explosion problem. This is especially true in the context of model checking SDL with its asynchronous message-passing communication, since chaotically sending and receiving messages immediately leads to a combinatorial explosion caused by all combinations of messages in the input queues.

Embedding Chaos, Natalia Sidorova and Martin Steffen,
In the Proceedings of the 8th International Static Analysis Symposium (SAS'01), Paris, 2001, © Springer-Verlag
(gzipped postscript, pdf), slides: pdf

introduces an automatic transformation yielding a closed system. By embedding the outside chaos into the system's processes, we avoid the state-space penalty in the input queues mentioned above. To capture the chaotic timing behaviour of the environment, we introduce a non-standard 3-valued timer abstraction. Data-flow analysis is used to detect instances of chaotic variables and timers and prove the soundness of the transformation, which is based on the result of the analysis.

We have implemented embedding chaos approach as a translatior from DTPromela to DTPromela (Dtp2dtp).

Download and Requirements

gzip -d promela.tar.gz

and extract the package "promela" with

tar xf promela.tar

Dtp2dtp is written in the Java language. It will run on any system that supports the version 1.2 of Java (or any later version).

Usage

To use Dtp2dtp, save list of external signals in some file, for example sig_ext, and

java promela/Dtp2dtp inputfile sig_ext outputfile

To try some examples download examples.tar.gz

If you have any problems with the tool, or want some more information, please write to Natalia Ioustinova: ustin@cwi.nl.