About Alloy¶
Alloy is a formal modeling language proposed by Daniel Jackson at MIT in the late 90s. Initially is was mainly tailored at describing software structures, but the latest Alloy 6 version also natively supports behavioral design. Alloy 6 is the version of Alloy used in this book.
Installing Alloy¶
Alloy models can be automatically analyzed with a tool called Alloy Analyzer that can be downloaded here. The Analyzer is implemented in Java and for most platforms the downloaded jar can be directly executed with the java -jar command. For macOS, a dmg installer is also available.
You can also try Alloy online in the Alloy4Fun web application. This online version allows the easy sharing of models with permalinks, and can also be used to share specification challenges in educational concepts. But it has some limitations when compared to the standalone Analyzer, namely in the validation of behavioral specifications. To learn more about how to use Alloy4Fun in education, read Experiences on teaching alloy with an automated assessment platform [SCP21].
Installing unbounded model-checkers¶
Alloy 6 already comes with embedded solvers and is therefore self-contained. However, it can optionally leverage so-called unbounded, or complete, model-checking to increase the breadth of verification (more on that in the Behavioral modeling chapter). Currently, Alloy 6 supports NuSMV (free/open-source) and nuXmv (proprietary, free for non-commercial or academic purpose): these tools must be installed in addition to Alloy (check their respective web pages for installation instructions). Provided they appear in the path of executable programs (PATH environment variable), they will be available as electrod.nusmv or electrod.nuxmv in the list of solvers available in the menu.
Alloy versions¶
The main novel feature in Alloy 6, when compared to previous versions of Alloy, is native support for behavioral design, namely the possibility to declare mutable structures and reason over these. The reader may wonder if the previous Alloy 5 version, where all structures were immutable, was useful in any way. In fact, in many software systems the main design problem concerns just structural aspects. This book starts precisely by explaining how Alloy can be used for structural design (in the Structural modeling chapter).
With Alloy 5, it was still possible to reason about behavior, by explicitly specifying the notion of time and of execution traces. However, this was often a rather time-consuming and error-prone task. The Electrum extension [FSE16] [ASE18] was proposed precisely to address this shortcoming. Electrum added an implicit notion of time, allowed the declaration of mutable structures, and the specification of properties with temporal logic. With Alloy 6, these extensions became a standard part of Alloy.
For an overview of Alloy 5, check Alloy: A Language and Tool for Exploring Software Designs [CACM19] by Daniel Jackson, or his book Software Abstractions: Logic, Language, and Analysis [MIT12].
Alloy extensions¶
Many extensions of Alloy were proposed in the past, that are not part of Alloy 6. To try them out, you should download the respective versions of the Analyzer. Note that most of these extensions were derived from Alloy 5, so they do not support the behavioral specification constructs of Alloy 6. Here is a non-exhaustive list of extensions:
Alloy*, an extension that supports the specification and analysis of higher-order constraints, and that can be used, for example, to implement program synthesis [FMSD19].
AlloyMax, an extension that supports the specification and analysis of problems with optimal solutions [FSE21].
DynAlloy, an extension for the specification of behavioral models using an idiom inspired by dynamic logic [FSE17].
QAlloy, an extension for the specification and analysis of quantitative requirements [FSE22].