CSSE 373 Formal Methods in Specification and Design

P2

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. 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. Please include images demonstrating your model and its operations. (Note that 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.

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.

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.