CSSE 373 Formal Methods in Specification and Design

P1

Administrative Details

Purpose: practice modeling a system using Alloy, develop a basic understanding of the major project for the course by modeling a portion of it

Please note: A big part of practical formal methods is having conversations with your client so that your model reflects what they really want. To give you practice with that, projects in this class are somewhat underspecified and require that you go somewhat beyond what is specifically covered in class. I look forward to helping you with that, which is why some class meetings are canceled for project work, but you need to ask for help.

Other details:

• You must work in teams of 2 or 3 on the projects.

• Your team has a Subversion repository for the projects. The repository URL is:

  http://svn.csse.rose-hulman.edu/repos/csse373-201130-projteamNN

  where NN is your assigned project team number.

• 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 should not 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. Your audience for the report is a fellow student who understands Alloy but is unfamiliar with the system you are modeling.

Please include images demonstrating your model and its operations. You can right-click on the visualizer window to save images.

To simplify my giving feedback, please include the full code of your Alloy model as a section in your report. Be careful that comments and constraints aren’t obscured by line breaks.

Your report should indicate how much time each time member spent on the project.

Rubric

I will evaluate your work using this grading rubric [pdf].

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.

Based on a previous problem description by Mark Ardis.