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

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 defined in "Using lightweight modeling to understand Chord". 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 correct. The models of the "base" version are:

Tutorial Promela Models

Promela is the language of the model-checker Spin. 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 techniques. This sequence of models has significant tutorial value, because it illustrates two important and subtle aspects of model-checking: