Case Studies

The following is a list of Alloy case studies done at MIT and other institutions. The symbols appearing after a case study's title designate the study as

• well-documented
• modelling a real-world artifact

MIT

• Analyzing Multicast Key Management Schemes

  Mana Taghdiri

  MIT, December 2002

  A framework for analyzing a class of key management schemes used in secure multicast. (PDF)

  • Mana Taghdiri and Daniel Jackson. A Lightweight Formal Analysis of a Multicast Key Management Scheme. Proc. of the 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems ( FORTE). pp 240-256, October 2003. LNCS 2767. (PS) (PDF)
  • Mana Taghdiri. Lightweight Modelling and Automatic Analysis of Multicast Key Management Schemes. MIT Masters Thesis, December 2002. (PS) (PDF)

• RBAC Schema Verification Using Lightweight Formal Model and Constraint Analysis

  John Zao, Hoetech Wee, Jonathan Chu, Daniel Jackson

  MIT, December 2002

  Assuring logical consistency among the specification of entities, relations and constraints in a role-based access control (RBAC) schema becomes increasingly important and urgent as the access control systems increase their spatial and temporal span. This paper reports an attempt to employ ALLOY, a lightweight modeling system with automatic semantic analysis capability, to verify internal consistency of RBAC schema as well as explicit manifestation of certain algebraic properties. (PDF)

• Railway Safety

  Daniel Jackson

  MIT, October 2002

  A policy for controlling the motion of trains in a railway system is analyzed. Gates are placed on track segments to prevent trains for colliding. What criteria should be used to determine when gates should be closed? (PDF) (ALS)

• Understanding Filesystem Synchronization Software and Policies

  Tina Nolte

  MIT, August 2002

  A model of a framework for discussion of filesystem synchronization and used the framework to study policies and behaviour of popular filesystem synchronizers. (PDF)

  • Tina Nolte. Exploring Filesystem Synchronization with Lightweight Modeling and Analysis. MIT Masters thesis, August 2002. (PS) (PDF)
  • Tina Nolte. Understanding Filesystem Synchronization Software and Policies. MIT, August 2002. (PDF)

• Central Registry

  Allison Waingold, Jon Whitney, Robert Lee

  MIT, February 2002

  A new design pattern that uses an implicit invocation scheme to decouple system components and allow dynamic reconfiguration of system behavior. (PS)

• Modelling and Analyzing a Peer-to-peer Protocol

  Daniel Jackson, Hoeteck Wee

  MIT, February 2002

  A small and compact Alloy model of Chord, a distributed lookup primitive for peer-to-peer systems. (PDF)

• Analyzing and Correcting an Intentional Naming Scheme

  Sarfraz Khurshid

  MIT, December 2001

  Lightweight formal modeling and automatic analysis were used to explore and correct the design and implementation of the Intentional Naming System (INS). (PDF)

  • Sarfraz Khurshid. Analyzing and Correcting an Intentional Naming Scheme. MIT, December 2001. (PDF)
  • Sarfraz Khurshid. Correcting a Naming Architecture Using Lightweight Constraint Analysis. RQE Report, MIT Lab for Computer Science, December 2001. (PS) (PDF)

• Air Traffic Control

  Gregory Dennis, Mandana Vaziri

  MIT, March 2001

  Explores new ideas for the design and analysis of air traffic control software systems.

Other Institutions

• Alloy model of Pacman

  David Faitelson

  An elegant model of how pacman moves around a mazes, avoids walls, eats food, and sometimes gets eaten by Blinky the ghost. The model is very readable, although there is not any explicit supporting documentation.
  (ALS)

• Using Alloy to Automatically Verify the Soundness of the Simulation Rules for Reasoning about State-Based and Event-Based Models

  Christie Bolton

  Oxford University Computing Laboratory, April 2003

  How Alloy might be used to automatically compare state-based and event-based systems, and in particular to reason about and compare models expressed in Z and CSP. (PS) (ALS)

• Modelling the Active Badge System

  Steven Xu

  Queen's University at Kingston, January 2003

  Alloy is used to model aspects of the Active Badge System -- a system that allows locating people carrying an Active Badge in a building. (PDF) (ALS)

• Checking and Reasoning about Semantic Web through Alloy

  Jin Song Dong, Jing Sun, Hai Wang

  National University of Singapore, September 2002

  Use of Alloy to analyze DAML+OIL ontologies. (PDF)

• Reference Model for Open Distributed Processing

  Andrey Naumenko

  LAMS, Swiss Federal Institute of Technology, October, 2001.

  A formalization of RM-ODP Part 2 using Russells Theory of Types, Set Theory and regular predicate logic. The formal model of RM-ODP Part 2 is written in Alloy:

  • Andrey Naumenko. Triune Continuum Paradigm: a paradigm for General System Modeling and its applications for UML and RM-ODP. PhD Thesis number 2581, Swiss Federal Institute of Technology - Lausanne (EPFL), June 2002. (PDF)
  • Andrey Naumenko and Alain Wegmann. RM-ODP part 2: Foundations in Alloy. EPFL-DSC technical report No. DSC/2001/041, August 2001. (PDF)
  • Andrey Naumenko and Alain Wegmann. A Formal Foundation of the RM-ODP Conceptual Framework EPFL-DSC technical report No. DSC/2001/040, July 2001. (PDF)
  • Andrey Naumenko, Alain Wegmann, Guy Genilloud, William Frank. Proposal for a formal foundation of RM-ODP concepts, Proceedings of ICEIS 2001, Workshop On Open Distributed Processing - WOODPECKER`2001, Setubal, Portugal, July 2001, pp. 81-97. (PDF)

• The NYC Subway Signaling System

  Anita Sarma, Adrita Bhor

  University of California, Irvine, March 2001

  A model of the interlocking of subway tracks, where in trains are routed to different tracks based on a routing algorithm and track availability. (DOC)

• A Formal Model of Addressing for Interoperating Networks

  Pamela Zave(AT&T Labs)

  Proceedings of the Thirteenth International Symposium of Formal Methods Europe, 2005.

  (PDF remote) (PDF local)

• Lessons Learned Using Alloy to Formally Specify MLS-PCA Trusted Security Architecture

  Brant Hashii

  Proceedings of the 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE'04). October, 2004. Washington DC, USA. Pages 86-95. ACM Press.

  (PDF)

• The NYC Subway Signaling System: An Alloy Case Study

  Anita Sarma and Adrita Bhor

  University of California, Irvine, March 2001.

  (DOC)

• Modelling the Active Badge System

  Steven Xu

  Queen's University at Kingston, January 2003

  (PDF) (ALS)

• Proposal for a formal foundation of RM-ODP concepts

  Andrey Naumenko, Alain Wegmann, Guy Genilloud, William Frank

  Proceedings of ICEIS 2001, Workshop On Open Distributed Processing - WOODPECKER`2001, Setubal, Portugal, July 2001, pp. 81-97

  (PDF)