Logical Models of Software

Abstract

Quality in software can't be added as an afterthought, by extraordinary efforts in testing or refactoring. It must be there from the start, by design. A modelling language can help you articulate design ideas and debug them before implementation, when mistakes are still cheap to fix.

Alloy is a modelling language based on logic: its models are just collections of logical constraints. The benefits of logic are: familiarity and simplicity; being able to write very partial descriptions; the ability to use different modelling idioms; and the economy of using the same language for a system and its intended properties. Alloy's analyzer simulates execution and checks properties of systems fully automatically; it can exhaust billions of cases in seconds.

In this talk, I'll show an example of a logical model in Alloy, and demonstrate the use of the analyzer to debug it. I'll talk about our experiences using Alloy in a variety of domains, and about our current projects enhancing Alloy's underlying technology and applying it to new kinds of problem.

Back to Distinguished Lecture Series - Fall 2002 / Spring 2003 Schedule