FM 2006

 
August 21 - 27, 2006
McMaster University
Hamilton ON, Canada

Submission Dates

Technical Papers, Workshops and Tutorials

Friday February 24, 2006

Posters and Tools, Doctoral Symposium

Friday May 26, 2006

 

Notification Dates

Technical Papers

Friday April 28, 2006

Workshops and Tutorials

Friday March 10, 2006

Doctoral Symposium

Wednesday June 14, 2006

Posters and Research Tools

Monday June 12, 2006


Contact Information

General Inquiries

General Chair

Emil Sekerinski

Program Chairs

Jayadev Misra,
Tobias Nipkow

Workshops Chair

Tom Maibaum

Tutorials Chair

Jin Song Dong

Tools & Poster Chair

Marsha Chechik

Industry Day Chairs

Volkmar Lotz,
Asuman Suenbuel

Doctoral Symposium Chair

Ana Cavalcanti

Augusto Sampaio

Jim Woodcock

Sponsorship Chair

Jürgen Dingel

T9 Alloy Modeling Language and Analyzer
Tutor:
Greg Dennis
Robert Seater
Affiliation:
MIT, USA
Date:
August 22, 2006
Time:
9:00-12:30, 2:00-5:30, 1/2hr break at 10:30 and 3:30
Location:
ITB 237
Format:
Full-day interactive lab. Participants encouraged to bring laptops with Alloy Analyzer already installed.
Updated slides can be found on the Alloy FM06 website. USB keys with a complete Analyzer installation will also be available.
 

Topic:

Alloy is one of few formal methods that enables its user to express rich structural properties of systems and mechanically check those properties for validity. It has been taught in at least nineteen universities around the world and serves as the foundation of a forthcoming book on software specification.

Alloy comprises three key elements: a logic, a language, and an analysis. The Alloy logic is a first-order logic with sets, relations, and transitive closure. The language is a simple and intuitive notation for expressing and structuring specifications in the logic. The analysis is embodied in the Alloy Analyzer, which mechanically checks properties expressed in the language for validity. The Analyzer performs an exhaustive search for a counterexample to a claimed property, within bounds that the user provides. If it finds a counterexample, the counterexample is guaranteed to represent a true violation of the property; however, the analysis can fail to find counterexamples when they require larger bounds for their detection. Nevertheless, in practice most counterexamples are found in small bounds.

Alloy is useful for modeling systems from a variety of domains. Unlike most formal methods, Alloy can easily express structural properties of systems. Such structural properties are crucial to expressing the correctness of linked data structures and data structure operations, which are pervasive in object-oriented software. Alloy is also conducive to modeling the behavior of abstract state machines, and users can apply the analysis to search for traces of state machines that violate a claimed property. The inherent non-determinism in Alloy allows distributed algorithms to be readily specified as well. The
Alloy Analyzer provides a wide array of visualization options, so regardless of the domain, simulations of systems and counterexamples to properties can be presented to the user in an intuitive way.

Objective:

In addition to the basics of Alloy, this full-day tutorial will introduce participants to a collection of common modeling idioms and patterns. After attending, participants will be able to construct and analyze simple Alloy models; researchers will be able to assess the applicability of Alloy to their problem domain; and educators should feel qualified to include Alloy in their teaching.

Prerequisites:

The tutorial presumes no prior knowledge of Alloy, only the basics of first-order logic and set theory.

Biography of Tutors:

Greg Dennis is a third year PhD. student with the Software Design Group in the Computer Science and Artificial Intelligence Laboratory at MIT. He has worked on the design and development of the Alloy language and analyzer, and he is currently using Alloy technology to check the conformance of software to declarative specifications. As a teaching assistant in an undergraduate software engineering course, he has lectured in weekly recitation, served as a mentor for team software projects, and participated with overall course development. His teaching experience also includes volunteer opportunities teaching software development to high school students in the greater Boston area and college and high school students in Ghana, Africa.

Robert Seater is a third year PhD. student with the Software Design Group in the Computer Science and Artificial Intelligence Laboratory at MIT. His research has focused on helping software designers and engineers analyze and understand software components at the design level. He has worked on improving the user experience building logical models and, more recently, on extending the Problem Frames approach for integrating software components into engineering projects. His teaching experience includes assistantships in a graduate formal methods course, in an undergraduate computer systems course, and with the John Hopkins Center for Talented Youth.

Greg Dennis and Robert Seater are the co-authors of the online Alloy tutorial.