Alloy is a structural modelling language based on first-order logic, for expressing complex structural constraints and behaviour. The Alloy Analyzer is a constraint solver that provides fully automatic simulation and checking. Alloy has been developed by the Software Design Group at MIT. The first Alloy prototype came out in 1997, and was a rather limited object modelling language. Later versions added quantifiers, higher arity relations, polymorphism, subtyping, and signatures (Alloy’s structuring mechanism). The performance and scalability of the tool have gradually increased. Much work has been devoted to user interface issues also, in particular in the development of a flexible visualization mechanism.
The Alloy Analyzer is essentially a compiler. It translates the problem to be analyzed into a (usually huge) boolean formula. This formula is handed to a SAT solver, and the solution is translated back by the Alloy Analyzer into the language of the model. All problems are solved within a user-specified scope that bounds the size of the domains, and thus makes the problem finite (and reducable to a boolean formula).
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 synchonization, 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.
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.
On our website, you’ll find a tutorial, reference manual, papers, and case studies. The discussion forum is a good place to ask basic and advanced questions of other users. Bug reports and suggestions to the MIT Alloy group can be directed to [email protected]
Sarfraz Khurshid (UT Austin) used Alloy in his Testera tool, which generates test cases automatically from representation invariants. Kevin Sullivan and David Coppit (Virginia) used Testera to find bugs in Galileo, a fault tree analyzer used by NASA. Mandana Vaziri (IBM) used Alloy to check Java methods against specifications; Mana Taghdiri (MIT) is extending this work with a method that infers specifications for called procedures automatically from their code.
Christie Bolton (Oxford) has used Alloy to discover refinement relations automatically. Marcelo Frias (Buenos Aires) is working on extending Alloy with dynamic logic. Paulo Borba (Recife) is investigating sound object model transformations using Alloy. Jin Song Dong (Singapore) has developed techniques for applying Alloy to web ontology reasoning. Lee Momtahan (Oxford) is developing a mathematical theory that will allow inferences about unbounded cases to be inferred from Alloy’s finite analysis. Chris Wallace (Bristol) has applied Alloy to business process modelling. Susan Stepney (York) is investigating mutation testing of Alloy models. Robert Seater (MIT) is looking at ways to help novices understand models by generating examples and non-examples. Felix Chang (MIT) is extending model checking technology with Alloy-like data structuring. Pamela Zave (AT&T) has used Alloy for modelling networks and telephone switching features. Dewayne Perry and Sarfraz Khurshid (UT Austin) are using Alloy for analyzing software architectures. Maria Nelson (Waterloo) used Alloy to explore axioms of geometry.
Alloy is an attractive teaching tool, for two reasons. First, the language is very close to first order logic with relational operators. The syntax and semantics are very simple and uniform. The latest version improves on its predecessor in this respect: the language semantics is now untyped, so it can be explained without reference to types, and the language is more flexible (but at the same time the type checker itself is actually more powerful!). Second, the Analyzer gives students immediate, concrete feedback; the graphical display seems to help a lot too.
Alloy has been taught in courses at about 15 universities worldwide, in most cases as one of two or three approaches, including: Michigan State (by Laura Dillon), Imperial College (by Michael Huth), National University of Singapore (by Jin Song Dong), University of Iowa (by Cesare Tinelli), Queen’s University (by Juergen Dingel), University of Waterloo (by Joanne Atlee), Worcestor Polytechnic (by Kathi Fisler), University of Wisconsin (by Somesh Jha), University of California at Irvine (by David Rosenblum), Kansas State University (by John Hatcliff and Matt Dwyer), University of Southern California (by Nenad Medvidovic), Georgia Tech (by Colin Potts), Politecnico di Milano (by Carlo Ghezzi), University of Washington (by Rob DeLine), Auckland (John Hamer). The courses at Kansas State, Imperial and Politecnico di Milano include several weeks’ worth of material on Alloy, and the latest version of the textbook by Michael Huth and Mark Ryan (Logic in Computer Science: Modelling and reasoning about systems; Cambridge University Press) includes a chapter on Alloy. At MIT, we have found that students can learn Alloy in a few weeks with only limited background in discrete maths.
Z was a major influence on Alloy. Very roughly, Alloy can be viewed as a subset of Z. Unlike Z, Alloy is first order, which makes it analyzable (but also less expressive). Alloy’s composition mechanisms are designed to have the flexibility of Z’s schema calculus, but are based on different idioms: extension by addition of fields, similar to inheritance in an object-oriented language, and reuse of formulas by explicit parameterization, similar to functions in a functional programming language. Alloy is a pure ASCII notation and doesn’t require special typesetting tools.
Alloy is similar to OCL, the Object Language of UML, but it has a more conventional syntax and a simpler semantics, and is designed for automatic analysis. Alloy is a fully declarative language, whereas OCL mixes declarative and operational elements. The ‘navigational dot’ of Syntropy is a key operator in Alloy, but is given a more uniform and flexible interpretation than in OCL. Because operators can be applied to entire sets and relations, Alloy tends to be more succinct than OCL. Alloy models can describe object models and operations, as well as properties to be checked. The Alloy Analyzer can check the consistency of an object model expressed in Alloy, and can generate snapshots from it, and can execute operations and check their properties. Alloy can handle relations with arbitrary arity, and has structuring mechanisms to allow reuse of model fragments.
The Alloy Analyzer is, technically speaking, a ‘model finder’. Given a logical formula (in Alloy), it attempts to find a model – a binding of the variables to values – that makes the formula true. For simulation, the formula will be some part of the system description. If it’s a state invariant INV, for example, models of INV will be states that satisfy the invariant. If it’s an operation OP, with variables representing the before and after states, models of OP will be legal state transitions. For checking, the formula is a negation, usually of an implication. To check that the system described by the property SYS has a property PROP, you would assert (SYS implies PROP); the Alloy Analyzer negates the assertion, and looks for a model of (SYS and not PROP), which, if found, will be a counterexample to the claim.
Version 4.x uses a new model finder engine called Kodkod and has a revised visualizer. Read more about it here.
Version 3.0 improves on version 2.0 in a number of ways. Read more about it here.
Version 2.0 improves on the previous version in many ways. The language has support for arbitrary arity relations, relational operators, and basic integer operations. It has a new structuring mechanism for incremental extension, and a module system for dividing a model into separate files. It has parametric polymorphism for defining generic types and operations. The accompanying Alloy Analyzer is completely new. It offers better performance and scalability (through improved formula transformations, and the use of more powerful SAT solvers, such as MiniSat, zChaff, and Berkmin). The visualization facility is more flexible.
The motivation for the Alloy project was to bring to Z-style specification the kind of automation offered by model checkers. The Alloy Analyzer is designed for analyzing state machines with operations over complex states. Model checkers are designed for analyzing state machines that are composed of several state machines running in parallel, each with relatively simple state. Alloy allows structural constraints on the state to be described very directly (with sets and relations), whereas most model checking languages provide only relatively low-level data types (such as arrays and records). The input languages of model checkers do not usually allow you to describe the state with the kinds of data structure easily handled by Alloy (tables, trees, etc); most require even simple data structures to be encoded using low-level primitives such as arrays and enumerations.
Model checkers do a temporal analysis that compares a state machine to another machine or a temporal logic formula. The term ‘model checking’ refers to checking that a particular state machine is a model (mathematically speaking) of a temporal logic formula. Technically, the Alloy Analyzer is a model finder, not a model checker: given a logical formula, it finds a model of the formula.
Every model checker has some kind of state machine idiom built in. Alloy has no built in idiom. This makes it possible to express and check properties that cannot always be checked with model checkers, especially those that relate states at different points in an execution (for example, that two operations commute). By modelling traces explicitly in Alloy, you can check LTL properties; this amounts essentially to bounded model checking, and works well only when counterexamples can be found in small traces.
Most model checkers do not allow state transitions to be specified declaratively: the input is essentially a program that uses assignment statements to describe a transition step. The Alloy Analyzer is designed for declarative specifications, in which invariants and operations are described by arbitrary formulas that may involve conjunction pervasively. This is very important for software modelling, because it allows very partial models to be analyzed (and thus incremental analysis of a model during its construction).
The Alloy Analyzer’s analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It’s a “refuter” rather than a “prover”. When a theorem prover fails to prove a theorem, it can be hard to tell what’s gone wrong: whether the theorem is invalid, or whether the proof strategy failed. If the Alloy Analyzer finds no counterexample, the assertion may still be invalid. But by picking a large enough scope, you can usually make this very unlikely.
The choice of SAT solver can be set in the Alloy Analyzer’s preference panel. For most analyses, the choice of the SAT solver doesn’t matter. MiniSat and ZChaff are good choices for small problems; for larger problems, Berkmin seems to perform best.
Yes, you can use the mouse to right click on the diagram, then choose “export” to export it as a PNG or PDF file. (For single-button mouse users, you can hold down the Control key then click).
Alternatively, you can click the Dot button on the toolbar to see the textual representation of the diagram; simply copy & paste the text into a text file, then you can use the dot program in GraphViz to generate PS, EPS, JPEG, GIF, and many other output formats.