of Alloy and Spin
What Is Lightweight Modeling?
Lightweight modeling means constructing small, abstract models
of the key concepts of a software system.
Lightweight analysis refers to verifying properties of a model
within a bounded domain automatically, by means of enumeration over
This is often called "push-button verification."
Lightweight modeling is a highly cost-effective
"Experiences with protocol description"
1st International Workshop on Rigorous Protocol
Engineering, Vancouver, Canada, October 2011)
recounts some of my experiences
with lightweight modeling, and some of the problems that arise when
protocols are designed without it.
My favorite technologies for lightweight modeling are the
Promela language and its LTL model-checker
and the Alloy language and its model-enumerating
Both tools are freely
available for a variety of platforms.
In the spring of 2010 I taught them in a course on Formal Methods in
Networking at Princeton University.
The notes for my four lectures are in
Lecture 22 March,
Lecture 26 March,
Lecture 29 March, and
Lecture 2 April.
Below you can find some larger models with tutorial value.
Modeling and analysis with Alloy and Spin have
yielded many insights
on the correctness of
In addition, this in-depth study has led to some new and interesting
comparisons between Alloy and Spin (as a representative of model-checking).
The results, including the surprising observation that Alloy may be
better for verifying some network protocols than model-checking, are
"A practical comparison of
Alloy and Spin" (Pamela Zave; Formal Aspects of Computing
Tutorial Alloy Models
The paper above discusses three versions of Chord.
The original version comes from the Chord SIGCOMM paper, with
borrowing from another paper to fill gaps.
A model of the original version is:
The "best assembly" version was
"Using lightweight modeling to understand
It was obtained by assembling the best pieces, including both pseudocode
and text, from three published Chord papers.
The models of the "best assembly" version from this paper in Computer
Communications Review are:
The "base" version is a new version of Chord that has been proven
The models of the "base" version are:
Tutorial Promela Models
Promela is the language of the
These models of a point-to-point networked channel include the private
control states at each end of the channel.
Each model includes detailed documentation about what is
modeled, what properties it is expected to have, and how Spin was used to
verify those properties.
There is a sequence of four models, in the following order:
They form a sequence because each model after the first builds on its
predecessor. In each subsequent model, new aspects are added. To keep
the model simple enough to understand and analyze, some previous aspects--
already well-understood--are removed. A model with different aspects
typically has different properties and may require different verification
This sequence of models has significant tutorial value, because it
illustrates two important and subtle aspects of model-checking:
Verification employs approximately 16 different modeling techniques and
Spin features, some of them very poorly documented. It is easy to run a
model checker, but not always easy to understand what the output means.
These models can help a student appreciate the relationship between the
property to be verified and the technique needed to verify it. These
models can also keep students from being misled by the magic of
meaningless push-button verification.
When one is trying to apply model-checking to anything real, it is very
easy to become frustrated by state explosion. For example, a single
model with all the behaviors in this sequence of models would be
impossible to verify. This series illustrates how overall behavior can
be decomposed and abstracted to get a set of meaningful AND tractable
models that achieve the overall goal.