*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
the domain.
This is often called "push-button verification."
Lightweight modeling is a highly cost-effective
design tool.
"Experiences with protocol description"
(Pamela Zave;
*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 Spin, and the Alloy language and its model-enumerating Alloy Analyzer. 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
the Chord
ring-maintenance protocol.
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
summarized in
"A practical comparison of
Alloy and Spin" (Pamela Zave; *Formal Aspects of Computing*
27:239-253, 2015).

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:

- Alloy: chordfull.als.

- Alloy: chordbestccr.als
- Spin: Run chordbestccr.pml and chordbestccr.c according to the instructions in spindocu.txt.

- Alloy: chordbase.als
- Spin: Run chordbase.pml and chordbase.c according to the instructions in spindocu.txt.

- 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.