Tuesday, November 19, 2002
8:30 am - 12:00 noon

Micromodels of Software: Modelling and Analysis with Alloy

Daniel Jackson
Department of Electrical Engineering & Computer Science
MIT

Abstract

This tutorial will present a new approach to modelling using the technology of the Alloy language and analyzer. A micromodel is a tiny model, focusing on an aspect of a system that is risky -- because it is inherently complex, hard to get right, or central to the system, for example.

Alloy is a new modelling language designed to support lightweight, precise modelling of software systems. It combines the precision and unambiguity of formal specification languages with the flexibility and ease of use of rapid prototyping. It is a minimal extension of first order relational logic. The language itself is very small, but can succinctly express complex properties of software, particularly those involving structure and its evolution.

The Alloy Analyzer provides fully automatic analysis of Alloy models using new technology based on SAT solvers. A model can be simulated or checked for particular properties over a huge space of scenarios (often 1030 or more). For most analyses, it responds in seconds and thus provides feedback during model development. It requires no user intervention or test cases: the user merely gives the 'scope' -- the dimensions of the space to be searched.

Alloy has been taught in graduate courses at over a dozen universities, in the US, Canada, England, and Italy. It has been applied to the analysis of security systems, network protocols, file synchronizers, software architectures, distributed algorithms, name servers, etc.

Topics will include a full description of Alloy and sample applications. An informal session following the tutorial will provide an opportunity for hands-on experience building and analyzing a small model.

The tutorial should be of interest to reseachers working in the areas of modelling, specification and analysis; to teachers interested in finding new, more interactive ways to teach modelling; and to developers looking for better ways to explore and document designs.

More information about Alloy is available at http://sdg.lcs.mit.edu/alloy

Presenter Biography

Daniel Jackson is an Associate Professor of Computer Science at MIT, and the Ross Career Development Professor of Software Technology. He received an MA from Oxford University (1984) in Physics, and his SM (1988) and PhD (1992) from MIT in Computer Science. He has been a software engineer for Logica UK Ltd. (1984-1986), and has worked for several large corporations, including AT&T, Digital and Fujitsu. He was Assistant Professor of Computer Science at Carnegie Mellon University (1992-1997), and has been Associate Professor at MIT (since 1997). He is an editor of ACM Transactions on Software Engineering and Methodology, and has served on the programme committee of more than 20 international conferences, including FSE, ISSTA, OOPSLA, TACAS, and CAV. He has broad interests in several areas of software construction, including design, specification, development methods, and automatic analysis of designs, specifications and code.