CPOR-Spin: Spin with Clustered Partial Order Reduction
Contents
General Description
-
CPOR-Spin is an extension of Spin which exploits the hierarchy of
the verified system for more efficient verification. In standard Promela,
the model of the system is given as C-like "flat" composition of processes.
However, in reality, we deal more often with systems that exhibit significant
degree of hierarchy by Pascal-like nesting of the system components. CPOR-Spin
benefits from such a model structure via an improved version of the standard
partial order reduction algorithm, called Clustered Partial Order Reduction
(CPOR).
(CPOR improves the standard POR by using more refined notion of action
safety. More particularly, the standard Promela binary notion of
safe-unsafe, is replaced with several levels of safety, derived using the
Pasacal-like scoping of variables. As a consequence, the computing of the
ample set differs from the standard algorithm: the ample set can consist
of actions of several porcesses which are safe according to the new refined
definition.)
-
The intuition and the theory behind CPOR is described in:
T. Basten,
D. Bosnacki, "Enhancing Partial-Order Reduction via Process Clustering",
16th IEEE Conference on Automated Software Engineering ASE 2001, IEEE Computer
Society Press, 2001.
For a short description of the tool and the implementation see:
T.
Basten, D. Bosnacki, M. Geilen, "CPOR-Spin: Spin with Cluster-based Partial
Order Reduction", submitted, 2003.
-
We are aware of the following incompatibilities between CPOR-Spin
and standard Spin:
-
CPOR-Spin does not support dynamic creation of processes,
-
communication channel variables are not real variables, i.e., they
can be used only as named constants.
Apart from the above, CPOR-Spin should be fully compatible with the
standard version of Spin.
Download
Installation of CPOR-Spin is the
same as for standard Spin. Although so far CPOR-Spin has been tested
only under SunOS and Linux, it should be portable to all platforms on which
the standard distribution runs (i.e. all sorts of Unix and Windows platforms).
#define CPOR
in comments.)
Usage
-
You can use CPOR-Spin is the
same way as standard Spin. For instance, if you want to try some of
the examples above, say Simple.2, you should first generate the special
purpose verifier - a set of C files (the main file being called pan.c),
with
spin -a Simple.2
Then the obtained C files should be compiled into an executable, for instance
with,
gcc -DSAFETY -DNOFAIR -DCPOR -o pan pan.c
Note that the only difference with the standard use is that the new compile
option -DCPOR must be used in order to activate the CPOR algorithm.
Also, when you use CPOR, the option POR should be on, i.e., if you use
-DNOREDUCE,
then CPOR will be also disabled.
The last phase is to execute the verifier by typing
pan
CPOR-Spin can be also used from xspin (version 3.2.4)
in the same
way as standard Spin. In order to activate the CPOR algorithm one should
add -DCPOR in the Advanced Verification Options/Extra Compile-Time
Directives. Mind that in order CPOR to take effect the partial order reduction
should be on.
If you have any problems with the tool, or want some more information,
please write to Dragan Bosnacki: dragan@win.tue.nl.