Thursday 13:00-13:45 – Convention Ctr - Exhibit Hall 4A
Friday 12:00-12:45 – Convention Ctr - Exhibit Hall 4A

19 The Alloy Analyzer

Daniel Jackson
MIT Lab for Computer Science, dnj@mit.edu
Ilya Shlyakhter
MIT Lab for Computer Science, ilya_shl@mit.edu
Manu Sridharan
University of California, Berkeley, manu@alum.mit.edu

We propose a demonstration of the Alloy Analyzer(http://sdg.lcs.mit.edu/alloy/), a tool for building and verifying specifications of software systems. Our specifications are written in Alloy, a modelling language designed to be high-level and easy to understand while remaining amenable to automatic analysis. Alloy has a much simpler semantics than OCL, the Object Language of UML, and the Alloy Analyzer can automatically check correctness properties of Alloy specifications, catching serious conceptual errors very early in the software development process (no comparable tool exists for OCL). Previous versions of the Alloy Analyzer have been used to identify bugs in several published software systems. Also, a paper on using the Alloy Analyzer technology to check properties of object-oriented programs will be presented in OOPSLA 2002’s technical program.

The latest version of the Alloy Analyzer was built using the Java language and the Swing GUI library. To analyze a correctness property of an Alloy specification, the tool compiles the property and specification to a boolean formula, such that a satisfying assignment to the formula corresponds to a violation of the property. Novel techniques are employed to minimize the complexity of the generated formula, and an off-the-shelf SAT solver is used to search for satisfying assignments. The tool also provides a flexible visualization system for the property violations it finds, utilizing the AT&T Graphviz graph layout library. We plan to present an interactive demonstration of the analyzer, showing how a specification can be developed, analyzed, and debugged using the tool.