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.

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

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

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: