Plan
Department of Computing and Information Systems SWEN90004 Modelling Complex Software Systems
Concurrency Workshop 6, Week 7, Semester 1, 2021
Linear temporal logic
The purpose of this last workshop is to give you some experience with the use of LTL to describe model properties, and with the model checking functionality in LTSA that allows you to verify temporal logic properties of FSP models.
The exercises
1. We previously experimented with this definition of resource sharing:
RESOURCE = (acquire -> release -> RESOURCE).
USER = (acquire -> use -> release -> USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
Specify LTL formulae for the following properties, and use the LTS model checker to verify whether they are true or false:
(a) Both processes a and b eventually acquire the resource.
(b) It is always the case that if a process acquires the resource, it will eventually release it.
(c) It is always the case that if a process acquires the resource, it will not release it until the other process acquires it.
2. This example is from Magee and Kramer, Chapter 7. A single-lane bridge allows traffic to only flow in one direction at a time. To simplify the model, cars travelling left to right are red cars, and cars travelling right to left are blue cars. There cannot be both red and blue cars on the bridge at the same time. There can be multiple of a single colour, but they cannot pass each other. The following figure shows a snapshot of the single-lane bridge:
An FSP model for this is listed in the appendix. It is also available on the LMS in file single_lane_bridge.lts.
There are N cars of each colour. Cars of each colour enter the bridge in numerical order, and once N cars have entered, car number 1 is the next to enter. Specify formulae for the following properties of the single-lane bridge system, and use the LTS model checker to verify whether they are true or false:
(a) For all of the red cars, it is always the case that each car will eventually enter the bridge.
(b) For all of the red cars, it is always the case that if the car enters the bridge, it will eventually exit.
(c) There are never both blue and red cars on the bridge at the same time; that is, the bridge is safe.
3. Extend the traffic light example from Lecture 18 (Concurrent Processes in FSP) and create an intersection containing two traffic lights¡ªone going in each direction in the intersection¡ª such that the intersection is safe: when one light is green or yellow, the other should be red.
Verify that your model is indeed safe by specifying a LTL predicate and using the LTSA model checker.
Appendix: Single lane bridge model in FSP
/** From Ch 14: “Concurrency: State Models and Java Programs”
* Jeff Magee and Jeff Kramer
*/
/** Single Lane bridge
* – Red cars go from west to east
* – Blue cars go from east to west
*/
const N = 2 // number car types
range T = 0..N // car count
range ID = 1..N // car identities
BRIDGE
= BRIDGE[0][0], // initially empty
BRIDGE[r:T][b:T] // r is the red count, b the blue count
= ( when (b==0) red[ID].enter -> BRIDGE[r+1][b]
| red[ID].exit -> BRIDGE[r-1][b]
| when (r==0) blue[ID].enter -> BRIDGE[r][b+1]
| blue[ID].exit -> BRIDGE[r][b-1]
).
CAR = (enter -> exit -> CAR).
/* Cars may not overtake each other */
NOPASS1 = C[1],
C[i:ID] = ([i].enter -> C[i%N+1]).
NOPASS2 = C[1],
C[i:ID] = ([i].exit -> C[i%N+1]).
||CONVOY = ([ID]:CAR || NOPASS1 || NOPASS2).
||CARS = (red:CONVOY || blue:CONVOY).
||SingleLaneBridge = (CARS || BRIDGE).