dSPIN:
a model checker for programs
Overview
dSPIN is an extension of the SPIN
model checker that offers efficient means for the verification of concurrent
programs written in high(er)-level programming languages. It provides a
number of novel features implemented on top of standard SPIN's state space
exploration and reduction algorithms:
-
memory references (pointers);
-
dynamic memory allocation/deletion;
-
recursive functions;
-
function code references (function pointers)
-
garbage collection
-
symmetry reductions
The design of dSPIN is driven by the need
to enhance the expressiveness of existing modeling techniques, while coping
with potential complexity blow-ups caused by adding extra functionalities.
The input language of dSPIN is a superset of PROMELA containing a small
number of new constructs such as pointer type variables, memory allocation
statements, function definitions and invocations. Such constructs are supported
by both the random simulator and verifier generator. The tool is SPIN-backwards
compatible that is, every standard SPIN model can be also verified using
dSPIN instead.
Download
Related papers
-
R. Iosif and R. Sisto. "dSPIN: A Dynamic Extension
of SPIN". In Proc. of the 6th SPIN Workshop, LNCS 1680 pp. 261 --
276, (September 1999)
(PDF)
.
-
R. Iosif and R. Sisto. "Using Garbage Collection
in Model Checking". In Proc. of the 7th SPIN Workshop, LNCS 1885 pp. 20
-- 33 (September 2000)
(PDF)
-
R. Iosif. "Symmetric Model Checking for Object-Based
Programs". KSU CIS TR 2001-5 (PS.GZ)
-
R. Iosif. "Exploiting Heap Symmetries in Explicit-State
Model Checking of Software". In Proc 16th IEEE Conference on Automated
Software Engineering pp. 254 -- 261 (November 2001) (PDF)
-
R. Iosif. "Symmetry Reduction Criteria for
Software Model Checking". Proc. 9th SPIN Workshop on Software Model Checking
(to appear). (PS)
Updates
-
Version 0.2 (Jan 2000): Added garbage collection
algorithms. Some bug fixes on Linux.
-
Version 0.2 (Apr 2000): More bug fixes. Made
up an automatic test suite.
-
Version 0.3 (Mar 2001): Implemented a "light"
form of symmetry reductions.
-
Version 0.4 (Apr 2001): Canonical symmetry
reductions based on topological heap ordering.
Feedback
Please send any kind of feedback to: Radu.Iosif#imag.fr
(where # is @)
Last updated Apr 13 2001 by Radu
Iosif