ECE 450: Software Engineering II

Assignment 5 (Updated March 29, 2001)

Due: Wednesday, April 11 2001

If you have done Assignment 1 in a team, do this assignment INDIVIDUALLY. If you have done Assignment 1 on your own, you may do this assignment in a team.

In this assignment you will create and verify a controller for a simplified version of Towers That Be and simulate the resulting system. The architecture for this system was described in Assignment 2.

Part I

You are to specify and verify the behavior of a simple elevator system. The system consists of one elevator that services 2 floors of a very short apartment building. Each floor has a call button that a user presses to get the elevator to come to that floor and open its door. Inside the elevator, there is one destination button for each of the two floors; passengers press these buttons to get the elevator to go to a particular floor and open its door. If the elevator moves between floors, it should do so within 1 time unit (i.e., the elevator should not move for two consecutive states). Once the elevator arrived at a floor, it should stay there with its door open unless there is another request to use the elevator.

You are to specify the behavior of your elevator system in the SMV input language. The system should also satisfy the following properties, which you specified in CTL as part of Assignment 4.

• Calls to use the elevator are eventually serviced.
• Destination requests from inside the elevator are eventually serviced.
• The elevator never moves with its door open.

Using the NuSMV model checker, verify that your specification satisfies the above properties. See the end of this document for specific requirements to the model and to the documentation.

Part II

Now we will specify a somewhat more complex elevator controller. This system is a modification of the previous one, where

• There is an OpenDoor button, in addition to call and destination buttons of the elevator. If the OpenDoor button is pressed when the elevator is not moving, then the door should open (remain open) for an extra time unit, i.e., for an extra state. However, a user should not be able to keep the door open indefinitely if the elevator has other requests to service.
• The building now has four floors. As in Part I, the elevator takes one "time unit" to go between floors n and n-1 (n+1).

The following properties need to be re-written in CTL. Note that many but not all of these were given in Assignment 4.

• Calls to use the elevator are eventually serviced (even if OpenDoor button is being pressed).
• Destination requests from inside the elevator are eventually serviced (even if OpenDoor button is being pressed).
• The elevator never moves with its door open.
• The elevator should keep its door open until there is a request to use it.

Think of and add at least one more CTL property (not equivalent to the ones presented above) that is vital to the correct operation of your elevator system.

Using the NuSMV model checker, verify that your specification satisfies all of these properties.

Part III

Obtain from the newsgroup ut.ecf.ece450 the elevator simulation program written by Chhad Aul. Read the READ_ME file. Write a controller program (controller.c) for the Towers That Be (from Assignment 1) for 3 elevators and 9 floors. These numbers should be easily-changed constant definitions. To get an idea of how the interface to the simulator should look like, consult the supplied version of a simpler controller (provided in controller.c). This controller does not have the required elevator control properties. Test your program using actions that illustrate each of the properties of Part II. "Illustrate" does not mean "prove"; to illustrate that the door never opens when the elevator is moving, it is sufficient to show a single finite sequence of reasonable actions during which the door was not open whenever the elevator was moving.

Modeling/Verification/Simulation/Submission Instructions:

• Ensure that the model of the environment is given correctly, that is, there are no unnecessary constraints placed on the environment. For example, users should be able to press buttons at any point. In the accompanying document (see below), describe the assumptions you made about the environment and discuss why they are justifiable.
• Use FAIRNESS correctly. For each FAIRNESS statement, add a short statement describing why this fairness assumption is meaningful.
• Document your controller carefully, the way you would good software.
• For each CTL formula, describe its meaning in English in addition to giving the formalization. In addition, determine under what circumstances this formula can hold vacuously, and specify and verify an additional formula which guarantees that it does not happen.
• Submit a short report on each model, with assumptions about the environment (and why they make sense), some modeling decisions (including discussion of FAIRNESS, if appropriate), the properties you verified, and the time it took for verification. Include the additional property from Part II. Also include the size of your model, as returned by NuSMV.
• In this report, outline your experiences with NuSMV. In particular, discuss what did not work, what you found awkward, what suggestions for improvement you may have. In addition, discuss which aspects of Towers That Be would be hard to model and/or effectively verify with NuSMV.
• Include in your report the sequence of actions you used in Part III to illustrate each of the properties in Part II.
• Finally, since we have not used submit this year, please mail a tar file with your two models and controller.c to Benet (benet@cs.toronto.edu). We do not intend to run everyone's models and simulations, but may need to do this in select cases.