Plan
School of Computing and Information Systems SWEN90004 Modelling Complex Software Systems
Concurrency Workshop 5, Week 6, Semester 1, 2021
Safety and Liveness in FSP
This workshop should give you experience with specifying safety and liveness properties in FSP (in addition to some further practice specifying FSP models!)
The exercises
1. What action trace violates the following safety property?
property PS = (a -> (b -> PS | a -> PS) | b -> a -> PS).
Think about the set of traces that would be accepted under this property first, then try to identify the characteristics of those that wouldn¡¯t. Once you think you have worked it out, use LTSA to draw the LTS for this property.
2. A lift has a maximum capacity of ten people. In the model of the lift control system, passen- gers entering a lift are signaled by an enter action and passengers leaving the lift are signaled by an exit action. Specify a safety property SAFE LIFT in FSP which when composed with the lift will check that the system never allows the lift that it controls to have more than ten occupants.
Once you have specified the safety property, also implement two versions of the lift: LIFTv1, that triggers a property violation when composed with your safety property; and LIFTv2, that passes the LTSA safety check when composed with your safety property.
3. In an operating system, a binary semaphore is used to control access to the console. The console is used by user processes and system processes. Construct a model of this system and investigate the scheduling conditions under which user processes may be denied access to the console.
(Hint: the operating system is essentially a simpler version of the readers-writers problem from Lecture Con.09 in which only one process can ever have access at a time.)
4. Two warring neighbours are separated by a field with wild berries. They agree to permit each other to enter the field to pick berries, but also need to ensure that only one of them is aver in the field at a time. After negotiation, they agree to the following protocol.
When one neighbour wants to enter the field, he raises a flag. If he sees his neighbour¡¯s flag, he does not enter but lowers his flag and tries again. If he does not see his neighbour¡¯s flag, he enters the field and picks berries. He lowers his flag after leaving the field.
Model this algorithm for two neighbours N1 and N2. Specify the required safety property for the field and check that it does indeed ensure mutually exclusive access. Specify the required progress properties for the neighbours such that they both get to pick berries given a fair scheduling strategy. Are there any adverse circumstances in which neighbours would not make progress? What about if the neighbours are greedy and decide to wait for the other one to lower their flag first?
(Hint 1: The following FSP can be used to model the flags.)
const True = 1
const False = 0
range Bool = False..True
set BoolActions =
{setTrue, setFalse, check[False], check[True]}
BOOLVAR = VAL[False],
VAL[v:Bool] = ( setTrue -> VAL[True]
| setFalse -> VAL[False]
| check[v] -> VAL[v]
).
||FLAGS = (flag1:BOOLVAR || flag2:BOOLVAR).
(Hint 2: It may be simpler to start by specifying each neighbour process separately, rather than using process labelling)