MINI PROJECT (Monday, March 5 at 14:00 -- Sunday, March 18 at 23:59)
The VIP
The (mere mortal) neighbours
 |
-
"THE VIP ELEVATOR"
The VIP Elevator System® involves an appartment
building with five floors (a ground floor "G.", three
regular floors "1.", "2.", and
"3.", and the penthouse floor "P." for a
special person, known as "The VIP").
The appartments are connected to the ground floor (and to each
other) via an elevator (from the renowned ThyssenKrupp / Kone / Otis /
Schindler / Miltsubishi-Electric Elevator-production Cartel). The
elevator is running (up and down) inside an elevator
shaft and powered by a powerful motor (that may pull it upwards and
push it downwards any number of floors atomically "in one go"). The
elevator has a ceiling light that has three settings (on,
off, and dim). The elevator may be called to a
particular floor when a person presses one of the "elevator call
buttons". The elevator has a control panel with buttons
(conceptually, with the "same" buttons as those on the individual
floors; i.e. just imagine that a person in the elevator can push those
buttons).
To ensure fairness, the system is capable of storing up to
M=2 button presses that are then to be processed according
to the order in which the buttons were pressed (maybe not the most
efficient way to process elevator requests, but let's not
worry about algorithmics). The elevator has a maximum capacity of
C persons, which may never be exceeded!
VIP Special Treatment:
The VIP doesn't like to mix with
his (mere mortal) neighbours. To this end, a few modifications to the
appartment building has been made. First, the VIP cannot be bothered
with pressing buttons to call an elevator, therefore his door has been
rigged with a call button, so that the elevator can be automatically
summoned when the VIP opens his door. Also, the VIP has his own
private "VIP-exit" (and "-entrance") door at the ground floor. The
neighbours dare not travel to the penthouse floor or use the VIP exit
(this may be assumed of their behavior).
Needless to say, the VIP does not like waiting, so this means
that the elevator should "get rid of" any persons inside and proceed
to handle the request of the VIP without unnecessary delays. In order
to achieve this, each floor of the appartment building has been fitted
with a turnstile (depicted as green "T"s); the ground
floor has two (one for the VIP, one for the neighbours). The
turnstiles serve two purposes: first, they make it possible to
calulate the number of people in an elevator; second, they may be made
to appropriately block access to the elevator.
Finally, the VIP doesn't like bright light, so the elevator ceiling
should be set to dim when the VIP is in the elevator. (However, the
neighbours want the light to be properly on when riding the elevator
and the light should be off when there are no-one in the elevator.)
|
Here's the FSP code for the VIP_DOOR_SENSOR and CALL_BUTTON:
 |
VIP_DOOR_SENSOR =
(door_opens -> VIP_DOOR_SENSOR).
CALL_BUTTON =
(call_elevator -> CALL_BUTTON). |
Feel free to modify the names of these actions (e.g. if you want to refer to specific people
entering/exiting) or completely remodel it.
Here's the FSP code for a TURNSTILE:
 |
TURNSTILE = TURNSTILE[FALSE],
TURNSTILE[locked:B] =
( lock -> TURNSTILE[TRUE]
| unlock -> TURNSTILE[FALSE]
|when (!locked) in -> TURNSTILE[locked]
| out -> TURNSTILE[locked]).
|
Again, you might wish to change the name of certain actions or completely remodel it. For instance, you may decide to operate with a variant turnstile that
has collapsed the lock and unlock actions into a single toggle action (that toggles between LOCKED/UNLOCKED
states).
|
NOTE
Underspecification:
Note that many questions are
underspecified (and thus left open for interpretation). It is your
job to identify possibilities, make appropriate (and realistic)
choices, and argue for them.
Damage control:
If you run short on time, modify and/or
simplify the problem (and explain what you have modified/simplified
and what consequences it has on the resulting system and/or properties
of the system). You may for instance decide to skip the Light (which
plays a lesser role in the system) or decide to restrict to
M=1. This will, of course, limit your potential grade,
but at least you get a system up and running.
|
YOUR TASK:
- Exercise 0: Read this page thorougly, as it is likely to indirectly improve your grade (in making sure you do not lose points by missing important information)!
- Assignment (specification --> model --> (safe) model --> (safe) implementation):
- a: Model the (unsafe)
VIP_ELEVATOR (i.e., without a controller).
- b1: Observe that too many people may walk into the elevator (i.e., causing the elevator to fall down).
- b2: Observe that the VIP may be forced to ride the elevator with his mere mortal neighbours (equally disastrous).
- c1: Add a safety property,
CAPACITY_EXCEEDED, formally verifying that the capacity may be exceeded.
- c2: Add a safety property,
VIP_NEIGHBOUR_MIX, formally verifying that the VIP may be forced to share the elevator with a mere mortal.
- d: Now add a controller to model a
SAFE_VIP_ELEVATOR (such that the above problems may no longer occur).
- e: Then verify formally that the above problems may no longer occur (with the controller constraining the behavior).
- f: Subsequently add a liveness property,
LIVE_VIP, formally verifying that the VIP is always eventually permitted to enter and leave his appartment (even in "rush-hour")); assuming the people always move.
- g: Make a structure diagram (excluding the above properties).
- h: Structure your model (into an implementation); i.e. give a UML diagram (same level of detail as in the UML-River.txt from the River hand-in; i.e. we do not want more elaborate UML annotations!).
- i: Finally, implement the
SAFE_VIP_ELEVATOR in Java (ideally using as many as the same names as in your model to emphasize model-implementation correspondence).
- Just use
System.out.println to "visualize" the behavior of the system
- If you want to make a GUI, it has to be implemented in separate classes (Note: this will not count towards your grade).
- Report: Document everything in a small written report which should (at least) include relevant discussions of all steps (a-i); including:
- explanations of your solutions and motivations for your solutions;
- discussion of relevant problematic issues;
- and arguments for your choices and solutions;
- in particular (for step a): an explanation of the meaning of all actions in terms of all processes;
- in particular (for step h/i): a discussion of the relationship between your model and your implementation (very important)!
- Note: the report should be self-contained in the sense that we should be able to understand your solution and the motivations for your solution
without having to look into the model/implementation! This means that it should for instance include all necessary and relevant parts of the model/implementation,
underlining relevant discussions in the report.
- Grading:
Be sure to motivate, explain, and argue for the reasoning behind your solution! Be concise and to the point (not necessarily "the more explanation the better"); include only issues relevant to the problem at hand (irrelevant issues may subtract points).
All this is what wins you the points (i.e. there are no/very few points for an unmotivated solution "out-of-the-blue", appropriate or not).
The actual grading is done relative to the course objectives; i.e., that you demonstrate the ability:
- to explain fundamental problems, techniques and solutions in the area of concurrency;
- to relate concrete models and programs;
- to reason about properties (correctness/safety/liveness) of concrete models and programs;
- to implement concrete models;
- to apply all above to create concrete models of systems
...whereever relevant. Note that I have only listed a subset of the competences from the Course Aim page here (the rest of the competences will be tested in the multiple choice test).
- Hand-in: send an email to
{besen@daimi.au.dk, brabrand@daimi.au.dk} (with subject "Mini-project: Group XX")
containing one attachment named groupXX.{tgz|tar.gz|zip} containing the following files (only):
report.{pdf|doc}:
- your report including a model structure-diagram and UML implementation-structure (for instance, in the appendix);
model.lts:
- your model (containing all process definitions;
VIP_ELEVATOR, CAPACITY_EXCEEDED, VIP_NEIGHBOUR_MIX, SAFE_VIP_ELEVATOR, LIVE_VIP, ...);
*.java:
- your implementation (with your comments, no IDE autogenerated comments); i.e., no
.class/.jar/build.xml/IDE-log/... files
|
|
