## January 19, 2012

Introduction
In this assignment, you will learn how to use the UPPAAL tool for modeling, simulation, and verification, and then design your own solution to a simple problem.

You may work with ONE other student on this assignment, but you must each turn in your own submission, as described below.

If you need help, ask a member of the instruction staff, or consult one of these online resources:

Before You Begin

Once you've done that, start UPPAAL and you should see the main window open up after a few seconds.

Part 1: Implement a model (10 points)
Implement the car/driver model that was discussed in class. The specifications are as follows.

• The Driver can either press the brake or press the accelerator.
• The Car is initially stopped (speed == 0).
• When the Driver presses the accelerator, the Car's speed increases by 10. However, if the speed is already greater than or equal to 100 and the Driver presses the accelerator, the speed does not change.
• When the Driver presses the brake, the Car's speed decreases by 10. However, if the speed is already zero and the Driver presses the brake, the speed does not change.
To implement this in UPPAAL, follow these steps:

First, in the main drawing area, select the Add Edge tool on the icon bar (with the picture of the little arrow, second from right) and draw a transition from the start state (the one with concentric circles) back to itself. To do this, after you select the Add Edge tool, click on the start state, click out in "space" somewhere, click somewhere else in "space", and then back on the start state.

Now go back to the icon bar and choose the Pointer tool (big green arrow), and double-click on the transition you just created. In the Edit Edge dialog box, enter "brake!" (without the quotes) into the Sync field, and click OK.

Repeat the above steps to create a transition from the start state back to itself, but this time with "accel!" as the Sync for the edge.

Rename this diagram by changing "Template" to "Driver" in the Name field (above the drawing area). Then save your work by clicking the Save button on the icon bar, or pressing Ctrl-S.

Now create a new drawing by choosing Edit on the menu and then Insert Template. Create the model for the Car that was discussed in lecture (and is described above). Double-clicking on a node (state) will allow you to edit its name and invariants. Double-clicking on an edge (transition) will allow you to edit the conditions on which it will be taken (Guard), any messages it should listen for or send out (Sync), and any actions it should take (Update). Represent the car's speed with a variable called "speed" (without the quotes).

When you are done with the drawing, rename this diagram by changing "P0" to "Car" in the Name field. Be sure to save your work!

Now you need to declare the different variables that are used in your model. Click the Declarations document that is a child of the Project folder (on the left-hand side). Add the line "chan brake, accel;" (without the quotes) to declare the channels, and then "int speed;" on the next line for the car's speed.

Last, go to System Declarations under the Project folder, and change "Process = Template();" to "car = Car();" and then add "driver = Driver();" on the next line. Then modify "system Process;" to "system car, driver;"

Before you attempt to simulate/verify your model, check for syntax errors by choosing Tools on the menu and then Check Syntax, or by pressing F7. The pane that displays syntax errors is hidden by default, but it's at the bottom of the drawing area. Just click the little "up" button or drag it up to display it. Fix any syntax errors you encounter.

Part 2: Simulate the model
Once you've finished drawing your car/driver model and checked for syntax errors, choose the Simulator tab. You should see a dialog about uploading the model; click "Yes".

The Enabled Transitions list in the top left corner shows all the possible transitions that can be taken at that point in the simulation. Because the car is initially stopped, at first you should only see "accel: driver --> car" as the only allowable transition (meaning, the driver sends the "accel" message to the car). Click the Next button beneath the Enabled Transitions list and you will see the state machine update itself.

Now you can step through the model by choosing a transition (most of the time, either pressing the accelerator or the brake) and clicking the Next button. You should also see the value of the "speed" variable listed in the middle pane. Simulate the model and convince yourself that it's working correctly before moving on.

Part 3: Verify the model (5 points)
Now choose the Verifier tab. The Overview lists all of the properties that have been created so far, and the Query list is where you enter properties.

Verify that the speed cannot go above 100 by clicking the Insert button on the right and entering "A[] speed <= 100" (without the quotes) in the Query box. Then click the Check button; you should see "Property is satisfied." in green letters at the bottom of the Status box. This is a safety property: it ensures that nothing bad can ever happen.

Verify that the car is able to (eventually) stop by clicking Insert again, then entering "E<> speed == 0" in the Query box, and clicking the Check button. This is a liveness property: it ensures that something good can eventually happen (recall from lecture that liveness properties usually would use A<>, but if you use A<> speed == 0, that won't work because the user may simply never hit the brake).

Last, verify that if the speed is zero, the car has stopped, using the property "speed == 0 --> car.stopped".

Save your query file in the same directory where you saved your model. You will need to submit both of these files (the .xml file and the .q files) as part of your lab assignment submission.

Part 4: Elevator problem (35 points)
In this part of the assignment, you will create and verify a model of a simple elevator controller. Here, though, the model of the user is a little more complicated, in that the user's possible actions are determined by her current state.

The file elevator.xml contains the skeleton that you should use for this part of the assignment. Note that a Person template has already been started for you. A Person has parameters "start_floor" (where they currently are) and "dest_floor" (where they want to go); these are specified as Parameters in the field above the drawing area. The Person also has a state machine that works as follows: Initially, the person presses the "call" button, and then moves to the "waiting" state. When the elevator door opens, the person gets in. She then chooses which floor she wants to go to, and presses the "close" button. While the elevator is moving, the person can either wait until the door opens, or she can press the "stop" button, at which point she will start panicking (yikes!) until the door opens. In either case, once the door opens, she gets out.

The Person template that we have provided is not finished! You need to figure out how to communicate the person's current floor and destination floor to the elevator (this is worth 5 points). You should not change the states in the diagram, or the messages that it sends and receives; you can, of course, add new states, transitions, and messages.

There is an empty Door template provided to you as well. Modeling the door is pretty easy, as it only has two states: "open" and "closed". When it receives a "close" message, it moves to the "closed" state; when it receives an "open" message, it moves to the "open" state (duh!). In the initial state, the door should be open. This part is worth 5 points.

The tricky part is the Elevator (15 points). Note that the floor that it starts out on is to be provided as a parameter called "current_floor". Its specifications are as follows:

• In its initial state, the elevator is not moving and the door is open.
• If the elevator receives a "call" message while it is not moving, it closes the door and then determines whether it needs to move up or move down to reach the floor to which it has been called. It then starts moving to that floor, one floor at a time. When the elevator reaches its destination, it opens the door.
• The door stays open until the person specifies which floor she wants to go to and presses the "close" button (notice that this is slightly different from modern elevators, of course!). The door closes, the elevator determines whether to move up or down, and starts moving in that direction. When it reaches its destination, the door opens.
• If, while the elevator is moving, the person presses the "stop" button, the elevator stops moving and opens the door, regardless of whether the destination floor has been reached.
Note that this model of the elevator is somewhat simplified, in that the elevator does not have to respond to any calls while it's already moving someone to their destination, and that the doors will open as soon as the person presses "stop", without checking that it has actually reached a floor. And, as noted, the user needs to press the "close" button to close the door. You can address those issues in your model for up to 5 total points of extra credit; if you do so, please make a note of it in your README file (see below).

There are lots of possible solutions for the Elevator. Think about its states before you start modeling it, and don't assume there is a one-to-one correspondence between the above specifications and the states/transitions in your model.

Hint: Don't forget to declare any global variables on the Declarations page (under Project). Also, remember to declare instance variables of your Templates in the System Declarations page. Because the Person and Elevator take parameters, you should declare them like "person = Person(5, 10);" meaning that the person is on the 5th floor and wants to go to the 10th.

Spend some time simulating the system to check that your Person is able to call the elevator, get in, move to the correct floor, and get out.

Last, verify the following safety and liveness properties (10 points) in the Verifier:

• It is possible for the person to eventually get out of the elevator.
• When the elevator is stopped, the door will eventually open.
• When the elevator is moving (up or down), the door will be closed.
• The elevator will eventually stop.
• It is possible for the person to eventually reach her destination floor, and the door will open.
Note: If the Verifier tells you that the property is not satisfied, go to the Options menu, select Diagnostic Trace, and then Shortest. Then go to the Simulator tab and you can step through a trace of your model showing the property being violated.

When you are done, save your model (.xml) and query (.q) files; you will need to include those as part of your submission, as described below.