Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik
Model Checker State Space Visualization
VMSSG exports
The following state spaces have been exported from the promela virtual
machine VMSSG,
written by Schürmans and Weber. The color of the node denotes the
SCC membership: A red node does not belong to an SCC (or, in terms of
Tarjan's algorithm, is a trivial SCC), whereas yellow and orange nodes
belong to an (alternatingly colored) SCC. The green transitions mark
the spanning tree explored in the DFS, red transitions mark forward
transitions to previously explored nodes, blue transitions mark back
transition (with respect to the position of the target node on the SCC
stack). The images have been traced with the POVRay raytracer, after being
layouted by an algorithm employed in the Walrus
graph visualization tool.
Download
A very premature version of the converter can be found here (276kB). It has a lot of
dependencies, uses Java 1.5, has a JNI lib included and is "very
beta", so be prepared. A short manual can be found here.
Gallery
The following example shows Peterson's mutual exclusion algorithm. The
model is provided within the SPIN distribution. Path reduction,
a completely statical analysis conducted prior to model checking by an
analyzer provided with VMSSG, reduces the state space to approximately
850 states, whereas the full model is yields 35000 states. The
following example has been generated for three processes. See the state explosion example gallery for
other sizes:
The next image shows a state space of the famous "two trains share one
bridge" model (c.f.
this skript, p. 125), here extracted from UML activity diagrams by the
HUGO
model checker. Again, static path reduction reduced the number of
states from 55000 to about 7000:
The next example illustrates the vast improvements of path
reduction. Both state spaces illustrate the second version of the
leader election protocol for three concurrent processes, as supplied
with SPIN. The left version was modified by the path reduction
provided with the VMSSG virtual machine, the right version shows the
unchanged model. The original model has 4571 states, the reduced model
just 677 states. No SCCs are found - the model terminates on every
run:
Conclusion: Path reduction works very well, but produces boring
results ;-)
The next example reaches the limits of displayability, and actually
took a full night to render on a pretty fast machine. It shows the
state space of the mobile1 model provided with SPIN, reduced by path
reduction. It yields 26663 states and 79197 edges. 51 SCCs are found,
and 7295 nodes do not belong to an SCC.
As a final example, this is the state space of a binary semaphore
example with three processes, where a strong fairness never claim is
used. This is a running example in my diploma thesis and the
developement of LWAASpin. In
discussing the (rather promising) results, a crucial question concerns
the presence of numerous SCCs of not too large size, so that Tarjan's
algorithm can be employed efficiently. I do hope that this image
illustrates that this hope is not entirely unfounded (althought I yet
fail to give a credible reason why the size and number of SCCs are
distributed in such a convenient fashion):
Further work
Despite the interesting shape of the state spaces, the usefulness of
those pictures is limited by the complete lack of state information
for the nodes. It is therefore desireable to have a specialized graph
viewer that can be used to navigate such a graph and investigate the
properties of interesting nodes - for example, "landmark nodes" that
have a lot of incoming edges.
Legacy
An old attempt at illustrating the state space of an ATM machine:
Contact
Back to my homepage.
Contact me at hammer "at"
pst.ifi.lmu.de.