Take Home Final - due Friday, March 19

Tasks you will need to do before starting:

• No new chapters to read; review of past chapters.

Resources you will need:

• Access to LTSA. Use this site to download: ltsa.jar. This should give you a jar file that is double-clickable.

Problem 1

Do exercise 8.1 (page 181). There are two parts. First, build the model and define some properties that make sense. Verify that the model satisfies the properties. Second, implement the room control station in Java. Note that you will have to also provide an interface to simulate the other components of the system. What you want is something like that in figure 8.12: (1) a GUI for the control station, and (2) a means to simulate actions of the other processes/components (see buttons on bottom). You should *not* try to build a full-simulation of the whole thing. Your goal is to prototype the control station app for a customer. Let the customer play around with it to see if they like it. Of course, part of your prototype is a means to simulate pieces of the system so the customer can see what is happening. Please see me if this is confusing.

What I would really like you to do is to think about how you might actually get from FSP to Java. Could you give a set of guidelines to a Java programmer on how to use an FSP model as a starting point? Perhaps get to a prototype and a set of test cases?

Turn-in: Turn in lts and Java program.

Problem 2

Modify your solution to exercise 2.6 so that it includes this property: "Once reset is activated, subsequent locks will be for decreasing station numbers until end is reached." In other words, you should guarantee that after reset if the radio locks on station x and then station y, then x>y. This will likely cause you to model stations - what I complained about in your first solution!

Turn-in: lts code.

Problem 3

Modify your solution to exercise 3.6 so that it has further detail as follows: Once the close action is taken, only departs are allowed. Once the museum is empty, turn on the alarm. When the museum opens, turn off the alarm. Now define a property: "When the alarm is on, the museum must be empty." Verify the property.

Turn-in: lts code.

Problem 4

This problem will focus on the cruise control problem of chapter 8. I notice that in some of my cars, the following constraint holds: it is not possible to resume if the current speed is too far below the target speed. I guess this is to avoid the car accelerating at a high rate. I would like you to model the cruise control system in enough detail to demonstrate this feature. There are two parts:

1. Build a model that includes the numeric speed of the car. You can either modify what is in chapter 8, or start from scratch. Use figure 8.2 as your basic guide. You can use constants and a range to specify pieces of the problem, e.g.,
   const TOO_MUCH = 5 //compare with (target - current)
   const TOP_SPEED = 15 //a slow car :)
   range SPEED_RANGE = 0..TOP_SPEED
   
2. Define a property (or assert) that captures the constraint. Show that it holds in your model.

Turn-in: lts code.