SPICED: Simple PROMELA Interpreter with
Crucial Event Detection
SPICED is an experimental model checking tool that implements the lattice theoretic techniques described in our paper: Producing short counterexamples using Crucial Events. SPICED is based on the SPIN implementation, and uses the same input language, PROMELA, to specify models.
Download
The tool, along with all the examples we have run it on, is available here.
SPICED produces error trails in the same format as SPIN. These error trails can be examined using SPIN's guided simulation feature (spin -p).
For now, SPICED only supports UNIX platforms (actually, was only tested on Linux).
You *MUST* gunzip and untar the distribution file in your home directory (wherever ~ redirects to).
Experimental Results
We ran SPICED on a large collection of PROMELA models from the BEEM database. Many models in the BEEM database contain errors injected into them, and specify the LTL properties to be verified on these models. For SPIN, the LTL properties were specified either in the form of simple assert() statements whenever possible, or as never claims. The "Model" column in the table below contains links to the PROMELA source for each of the models. The "Formula" column contains links to the CETL property specified in SPICED.
|
|
SPICED |
|
SPIN |
|||||||||
|
Model |
Time |
States |
Transitions |
Memory (MB) |
Formula |
Length of trail |
Trail reduction factor |
Time |
States |
Transitions |
Memory (MB) |
Length of trail |
|
0.014 |
99 |
90 |
3.147 |
39 |
67.56410256 |
0.018 |
1317 |
1320 |
2.622 |
2635 |
||
|
0.014 |
246 |
287 |
3.147 |
58 |
51.48275862 |
0.02 |
1492 |
1503 |
2.622 |
2986 |
||
|
0.03 |
6664 |
12605 |
3.454 |
74 |
413.8918919 |
0.125 |
15312 |
15792 |
4.606 |
30628 |
||
|
0.032 |
65387 |
141208 |
7.038 |
82 |
382.7926829 |
0.13 |
15692 |
16252 |
6.628 |
31389 |
||
|
0.016 |
16 |
9 |
3.147 |
8 |
18.875 |
0.009 |
74 |
81 |
2.622 |
151 |
||
|
0.016 |
16 |
9 |
3.147 |
8 |
18.875 |
0.01 |
74 |
81 |
2.622 |
151 |
||
|
0.018 |
17 |
10 |
3.147 |
9 |
24.88888889 |
0.01 |
110 |
121 |
2.622 |
224 |
||
|
0.018 |
18 |
11 |
3.147 |
10 |
29.7 |
0.01 |
146 |
161 |
2.622 |
297 |
||
|
0.018 |
18 |
11 |
3.147 |
10 |
29.7 |
0.01 |
146 |
161 |
2.622 |
297 |
||
|
0.018 |
18 |
11 |
3.147 |
10 |
29.7 |
0.01 |
146 |
161 |
2.622 |
297 |
||
|
0.019 |
19 |
12 |
3.147 |
11 |
33.63636364 |
0.01 |
182 |
201 |
2.622 |
370 |
||
|
0.018 |
2601 |
2658 |
3.249 |
510 |
1.97254902 |
0.019 |
2071 |
4412 |
2.622 |
1006 |
||
|
0.012 |
45 |
40 |
3.147 |
28 |
5.714285714 |
0.009 |
163 |
423 |
2.622 |
160 |
||
|
0.017 |
2257 |
3929 |
3.249 |
55 |
6.509090909 |
0.012 |
179 |
197 |
2.622 |
358 |
||
|
0.013 |
57 |
52 |
3.147 |
37 |
16.48648649 |
0.034 |
748 |
2397 |
2.622 |
610 |
||
|
1.226 |
401575 |
912557 |
25.573 |
158 |
8.303797468 |
0.018 |
656 |
701 |
2.622 |
1312 |
||
|
0.013 |
69 |
64 |
3.147 |
46 |
18.60869565 |
|||||||