CSSE 373 Formal Methods in Specification and Design

P1

Administrative Details

Purpose: practice modeling a system using Alloy

You may work in teams of 2 or 3 on the project.

Keep track of how much time you spend on this assignment. You will submit your solution as an Alloy model plus a report as a pdf file.

Problem Specification

Your company, Higher Expectations Ltd., makes lifts (elevators). Your job is to specify the control system for an installation that includes 3 lifts for 5 floors. Before you attempt to describe the complete system you need to specify a simple version that has only one lift and no floor call buttons:

  1. The lift has a set of buttons, one for each floor. These illuminate when pressed and cause the lift to visit the corresponding floor. The illumination is cancelled when the corresponding floor is visited by the lift.
  2. The lift has two arrows indicating future direction. One arrow is illuminated as the doors open. The illumination is cancelled as the doors close.

Tasks

Alloy Model

Write an Alloy model of the control system that includes:

  1. a signature representing the lift, with appropriate fields and auxiliary signatures to represent the lift’s current location and the state of its buttons, arrows, and doors
  2. any necessary facts to constrain your system (e.g., the up and down arrows are never both on)
  3. operation predicates (analogous to add and del for address books) that describe moving up/down one floor
  4. operation predicates that describe requesting/servicing a floor request.

Write appropriate predicates and commands to demonstrate your model and its operations.

You don’t have to specify the control algorithm that ensures that all requests are serviced. You just have to show that if the lift visits a floor for which there is a request then the illumination of that floor button is cancelled. (Write and check an assertion that demonstrates this.)

Be sure that your model is well documented, i.e., clear names for signatures, relations, predicates, etc., and comments describing constraints.

Report

Write a short report describing your model and the commands that you’ve included in it. Please include images demonstrating your model and its operations. (Note that you can right-click on the visualizer window to save images.)

Turn In

Turn in your work by committing your Alloy model and a pdf file of your report named P1report.pdf to your team subversion repository for this course.

Feedback

Each team member should complete the short, anonymous survey on ANGEL regarding this assignment. (I will study these surveys in detail after the conclusion of this offering of the course. If you have suggestions that you would like me to consider during this offering of the course, please tell me in person or use the separate Anonymous Suggestion Box on ANGEL.)

Based on a previous problem description by Mark Ardis.