Information about the exam
The exam consists of two parts:
- UML (domain model, sequence diagrams, use cases, application models, NO CODING). This part is similar to previous years and will give 30 points.
- Statecharts and TLA. This part gives 20 points. While there are many example of state chart exercises from previous years, the TLA part is new for this year.
According to the SIS, there is a minimum for passing the exam: "The minimum required score in the written exam is 20 out of 50 points. A score of less than 20 points in the exam will lead to a grade of F regardless of the number of points in the homeworks."
Grading of the second part
The state-based modelling using UML statecharts will be 12 points of the exam. You will submit an exported PDF from YAKINDU or MagicDraw. I recommend using Yakindu to make sure everything works, but the most important thing is to produce a clear and understandable statechart.
The remaining 8 points are for TLA. You should focus on modifying a system specification in order to check certain properties, see example below. Having TLA on your computer will be helpful, but not absolutely necessary: the counter examples you will be asked about can be solved by hand as well. Since this part is new, there is the possibility to earn extra credit to compensate points lost in the second part of the exam.
Example exercise
The format for the TLA exercise will be such that you are given an attempted model of a scenario and you will modify this to investigate potential problems. Here is an example exercise we discussed in the lecture. This is how it would look like in the exam.
Consider the following model of a cinema booking system. Each seat can either be free, booked, or purchased. Multiple users can use the system to first select the seats they want and then purchase the selected seats. (The variable variable sold is a ghost variable that is only needed to reason about the system. You may change it or add other such variables.)
------------------------------- MODULE cinema -------------------------------
EXTENDS Integers
CONSTANT Users, Seats
(* --algorithm cinema
variables
ticket = [s \in Seats |-> F],
sold = [u \in Users |-> {}]
define
F == "free"
B == "booked"
P == "purchased"
status == {F, B, P}
free_seats == {s \in Seats : ticket[s] = F}
booked_by == [u \in Users |-> {s \in Seats : ticket[s] = u}]
soldout == UNION {sold[u] : u \in Users} = Seats
consistent == \A u1, u2 \in Users : sold[u1] \cap sold[u2] /= {} => u1 = u2
end define
fair+ process user \in Users
variable select = 0
begin
Decide:
either
Book:
if free_seats /= {} then
with seat \in free_seats do
select := seat
end with;
BookTicket: ticket[select] := self;
end if;
or
Unbook:
if booked_by[self] /= {} then
with seat \in booked_by[self] do
select := seat
end with;
ReleaseTicket: ticket[select] := F;
end if
end either;
ProceedOrNot:
either goto Decide or goto Checkout end either;
Checkout:
either
Purchase:
ticket := [s \in Seats |-> IF s \in booked_by[self] THEN P ELSE ticket[s]];
sold[self] := sold[self] \cup booked_by[self]
or
Cancel:
ticket := [s \in Seats |-> IF ticket[s] = self THEN F ELSE ticket[s]];
end either;
NextCustomer:
goto Decide
end process
end algorithm *)
=============================================================================
Use TLA+ to answer the following questions.
- The most important safety condition for a booking system is that we do not sell the same seat to two different people. State this property formally in TLA notation.
- Create a model with two users and two seats. Run the model checker to check your property. It should be violated. Describe the counter-example trace.
- Use TLA to determine which operation MUST be atomic for the system to avoid double-booking: booking, unbooking, or both? (In other words, which labels must be removed: BookTicket, ReleaseTicket, or both?)
- The system services customers until tickets are sold out. Formulate the property that eventually all tickets will sell out in TLA notation.
Example solution
The best way to prepare for the exam is to solve this exercise yourself. Once you have solved it, you may click this button to compare...
\A u1, u2 \in Users : sold[u1] \cap sold[u2] /= {} => u1 = u2- This is a TOCTTOU race condition. The TLA checker gives the following example of how both users end up buying the same seat:
- User1 decides to book a ticket (goes to Book).
- User1 selects seat 1 (goes to BookTicket).
- User2 decides to book a ticket (goes to Book).
- User2 selects seat 1 (goes to BookTicket). This is possible because the database has not yet been updated by any of the users.
- User1 updates the database to book seat 1 (goes to ProceedOrNot).
- User1 then goes through the steps to purchase seat 1.
- User2 does the same.
- The only label we have to remove is BookTicket. We do not need to make the release atomic.
<>(UNION {sold[u] : u \in Users} = Seats). You should be able to add temporal properties to the model checker and check them, but this is not a very good example for liveness checking. If you just stare at the model, you can see that the user can just book and cancel forever. I will only ask for counter examples if TLA produces sensible ones.