Paper Authors

Abstract

NOTE: The first page of text has been automatically extracted and included below in lieu of an abstract

Experiences with Alloy in Undergraduate Formal Methods

Introduction

At the core of all engineering endeavors is the modeling of proposed system designs and the use of these models to determine system properties. While some models are physical, the vast majority use mathematics to both describe and analyze the consequences of design decisions. In the case of traditional engineering disciplines, most models are based on continuous mathematics, e.g., calculus and differential equations. The situation is quite different in software engineering, however, where the applicable models are more likely to be drawn from discrete mathematics, logic, and set theory. The term of art for such modeling approaches is formal methods.

One complaint about formal methods, voiced by both practitioners and students alike, is the lack of applicability to “real” problems. While some of these objections are undoubtedly based on an unwillingness to learn the relevant mathematics, this does not mean they can be dismissed out- of-hand. To be useful in practice, a modeling method must provide engineers with information that more than compensates for the cost of learning the technique and creating its models. Model checking is one formal method that has proven its value as a tool for describing and analyzing concurrency effects1,2. Alloy3,4,5, a modeling tool created by Daniel Jackson’s research group at MIT, provides similar value when modeling and analyzing the structural and behavioral consequences of software design decisions.

This paper reports on the value Alloy has brought to the undergraduate formal methods course within the software engineering program at RIT. The next section introduces Alloy by way of a well-known example problem, the birthday book6. This is followed by a section discussing the advantages Alloy for teaching undergraduates, especially as compared to traditional methods such as VDM7 and Z8. The final section discusses some areas where Alloy’s support for instruction needs improvement.

Birthday Book Example

Consider a system for maintaining a birthday book (that is, a book that lists birthdays for some set of persons); this example was originally presented in The Z Notation6. In Alloy, we would start by defining the necessary signatures: Named sets of indivisible, immutable, atomic objects and the relations that hold among these sets.

sig Person{} sig Date{} sig BirthdayBook { known : set Person, // those persons known in this book dates : Person -> Date // the birth day for each known person }

Here we have defined three signatures, Person, Date, and BirthdayBook, along with two relations, known and dates. The signature declarations implicitly state that the three underlying sets of atoms partition the universe of all atoms (that is, the three sets are pair-wise disjoint and

• Citation

• Format
  • APA
  • APA - LaTeX bibitem
  • MLA
  • MLA - LaTeX bibitem
  • Bibtex
  • EndNote - RIS

Lutz, M. (2006, June), Experiences With Alloy In Undergraduate Formal Methods Paper presented at 2006 Annual Conference & Exposition, Chicago, Illinois. 10.18260/1-2--1320