Alloy: A Logical Modelling Language

Abstract

Alloy, like Z, is a language for modelling software systems. Indeed, it draws many of its good ideas from Z: in particular, representing all data structures with sets and relations, and representing behaviour and properties with simple formulas. Unlike Z, however, Alloy was designed with automatic analysis in mind. A constraint solver based on reduction to SAT can check properties of Alloy models, and simulate execution (even of implicit operations). The key idea is to consider all possible bindings of a formula that assign no more than some small number of atoms to each given type. The result is a flexible mechanism that provides rapid and concrete feedback during evolution of a model. It cannot prove properties, but by exhausting all small test cases, it usually succeeds in finding bugs rapidly.

In my talk, I’ll explain the fundamental ideas underlying Alloy and its analysis: its basis in relation rather than sets, and the compromises (notably a restriction to first order structures and formulas) that make analysis possible. I’ll compare Alloy’s specification-structuring mechanism, the signature, to Z’s schema. I’ll illustrate some modelling idioms that we have developed in using Alloy, focusing on how mutation is represented. I’ll also show some examples of typical analyses, including a trace-based analysis that employs the idea of ‘machine diameter’ from bounded model checking to ensure that all reachable states are considered.

More information about Alloy can be found at http://sdg.lcs.mit.edu/alloy.