CSSE 373 Formal Methods in Specification and Design

P2

Administrative Details

Purpose: demonstrate the ability to model a system using Alloy and verify its mundane and essential attributes

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 practive 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. Here is an informal description of the expected behavior:

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. Each floor has 2 buttons (except the ground and top floors, which have only one), one to request an up-lift and one to request a down-lift. These buttons illuminate when pressed. The illumination is cancelled when a lift visits the floor and is either moving in the desired direction or has no outstanding requests. In the latter case, if both floor request buttons are pressed only one should be cancelled. The algorithm to decide which to service first should minimize the waiting time for both requests.
3. The lift has two arrows indicating future direction. One arrow is illuminated as the doors open. The illumination is cancelled as the doors close.
4. When a lift has no requests to service, it should remain at its final destination with its doors closed and await further requests.
5. Each lift has an in-service switch that is used to disable the lift during emergencies. When the switch is moved to “Off” the lift shall stop moving and cancel all pending requests. The lift is then “out of service”. When the switch is moved to “On” the lift becomes “in service”, and it should await further requests.
6. All requests for lifts from floors must be serviced eventually, with all floors given equal priority.
7. All requests for floors within lifts must be serviced eventually, with floors being serviced sequentially in the direction of travel.

Tasks

Alloy Model

Write an Alloy model of the control system that includes:

1. a signature representing lifts, with appropriate fields and auxiliary signatures to represent the lift’s current location and the state of its buttons, arrows, and doors
2. a signature representing floors, with appropriate fields and auxiliary signatures to represent the lift call buttons
3. any necessary facts to constrain your system (e.g., the up and down arrows are never both on)
4. operation predicates or event signatures that describe how the system changes with each time step
5. the control algorithm

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

Write appropriate assertions to demonstrate that your control algorithm satisfies the expected behavior. In particular, show that if a request is made it is eventually serviced.

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

Suggestions

• For your control algorithm, you will probably want to use a set of facts constraining the behavior. For example, if a lift reaches a floor for which there is a request, then the lift will open its doors; or a lift will keep going in its planned direction as long as there are requests remaining in that direction.
• You may use the provided solution to P1 as a starting point, though that is not required. If you use the provided solution you should provide credit/blame where it is due (e.g., “based on an original model by Curt Clifton”).
• Until you are confident in your solution, you will probably want to keep your scopes smaller than 5 floors and 3 lifts. You should increase to the specified scope for final checks.

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 P2report.pdf to your team subversion repository for this course.

Based on a previous problem description by Mark Ardis.