Questions

Unlike a programming language, an Alloy model is declarative: it can describe the effect of a behaviour without giving its mechanism. This allows very succinct and partial models to be constructed and analyzed. It is similar in spirit to the formal specification languages Z, VDM, Larch, B, OBJ, etc, but, unlike all of these, is amenable to fully automatic analysis in the style of a model checker.

Alloy has been used to model and analyze all kinds of system, but mostly with an emphasis on systems that involve complex structured state. Applications include: name servers, network configuration protocols, access control, telephony, scheduling, document structuring, key management, cryptography, instant messaging, railway switching, filesystem synchronization, semantic web. One area in which Alloy offers particular advantage over model checkers is for analyzing systems with configurations that are underdetermined, or that can change dynamically. For example, an analysis of the leader election phase of the Firewire prototol checked all behaviours involving all configurations of nodes (up to a certain size); a model checker would require that some configuration be hardwired.

In software engineering, one of the great benefits of Alloy is that you can analyze a tiny model. You can write three lines, and analyze it; add a few more lines, and analyze again. This incrementality makes Alloy especially good for exploring design ideas.