MINI PROJECT (Wednesday, March 8 at 15:00 -- Sunday, March 19 at 23:59)
-
"BANANA REPUBLIC"
A one-way road passes by the presidential palace in the "Banana Republic". In
order not to delay his excellency, El Presidente, and to make him avoid too close contact
with the population, a gate has been mounted (to the west) so
that access to the road may be restricted (by closing the gate). Underneath the gate is a
car entry sensor which detects cars passing by the gate when it is open. The road also has
a car exit sensor (to the east) which detects when cars exit the area in front of the palace.
The garage door of the palace is equipped with a sensor to detect when the presidential car
is leaving the palace; an entry sensor detects when it enters the main road, and a warning
signal (on/off) indicates whether or not cars are on the road (i.e., whether or not it is
safe for the president to enter the road).
You may assume that N=4 cars drive on the main road and that they "reappear" to the west
when they drive away to the east (as in the old PacMan games). Cars may overtake each other,
even in the crossing area (which has a capacity of, say, M=3 cars). You may also assume that
his excellency, El Presidente, only leaves the palace and that his car reappears at the palace
when he has driven off (to the east).
Your job is to make sure (using a controller) that no other cars are on the road in the area
in front of the palace at the same time as El Presidente's. The controller receives input
from the sensors and may control the gate (open/close) and warning indicator signal (on/off).
When El Presidente is nowhere in sight, the gate should be open so the cars may pass into the
restricted road without delay, however when El Presidente is coming, he should be allowed to
safely enter the road as soon as possible - even in congested rush-hour traffic.
|
Here's the FSP code for the SENSORS:
 |
CAR_ENTRY_SENSOR = (car_enter -> CAR_ENTRY_SENSOR).
CAR_EXIT_SENSOR = (car_exit -> CAR_EXIT_SENSOR).
GARAGE_SENSOR = (open_garage -> GARAGE_SENSOR).
|
Feel free to modify the names of these actions (e.g. if you want to
refer to specific cars entering/exiting) or completely remodel it.
Here's the FSP code for the GATE:
 |
GATE = OPEN,
OPEN = (close_gate -> CLOSED
|pass_gate -> OPEN),
CLOSED = (open_gate -> OPEN).
|
Again, you might wish to change the name of certain actions or completely remodel it.
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 --> (safe) model --> (safe) implementation):
- a: Model the (unsafe)
BANANA_REPUBLIC (i.e., without a controller).
- b: Observe that collisions with El Presidente can occur (i.e., give an erroneous trace).
- c: Add a safety property,
NO_CRASH, formally verifying that collisions with El Presidente can occur.
- d: Now add a controller to model a
SAFE_BANANA_REPUBLIC (such that collisions with El Presidente cannot occur).
- e: Then verify formally that collisions with El Presidente can no longer occur (with the controller constraining the behavior).
- f: Subsequently add a liveness property,
LIVE_PRESIDENTE, formally verifying that El Presidente is always eventually permitted to enter the restricted road even in congested rush-hour traffic.
- g: Make a structure diagram (not including 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_BANANA_REPUBLIC 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
{andersen@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; BANANA_REPUBLIC, NO_CRASH, SAFE_BANANA_REPUBLIC, and LIVE_PRESIDENTE);
*.java:
- your implementation (with your comments, no IDE autogenerated comments); i.e., no
.class/.jar/build.xml/IDE-log/... files
|
 |
Note: In addition, there will be a small extra exercise in "CCS and Process Equivalence" which is specified below:
|  |
PROCESS EQUIVALENCE EXERCISE (Posted March 15 at 16:30)
- -) Let "sim" be the simulation relation on processes; i.e. P sim Q if and only if P simulates Q.
P simulates Q if and only if every time Q can make an alpha-action resulting in process Q', then P can simulate this by making
an alpha-action resulting in a process P' such that P' simulates Q'.
This induces a Simulation Game which is the same as the bisimulation game, except that the attacker always
has to attack on the right-hand-side process and the defender on the left-hand-side process.
- a) Is sim an equivalence relation (why/why not)?
- b) Consider the processes: S and T:
- b1) Do we have that S sim T; why/why not?
- b2) Do we have that T sim S; why/why not?
- b3) Do we have that S teq T (i.e. are they trace equivalent (traces(S) == traces(T))); why/why not?
- c) Do we have that (for all choices of processes P and Q): if P and Q simulate each other, then P and Q are bisimilar; why/why not?
- i.e., forall P,Q: ((P sim Q) && (Q sim P)) => (P bisim Q)
- d) Do we have that (for all choices of processes P and Q): if P and Q are bisimilar, then P and Q simulate each other; why/why not?
- i.e., forall P,Q: (P bisim Q) => ((P sim Q) && (Q sim P))
- e) Do we have that (for all choices of processes P and Q): if P and Q are trace-equivalent, then P and Q are bisimilar; why/why not?
- i.e., forall P,Q: (P teq Q) => (P bisim Q)
|
|
