Our goal is to get a first hand at formal verification of real-time systems using the UPPAAL model-checker. We will review several notions:
Lien vers les transparents du cours
The goal of this first part is to review the main features of the tool UPPAAL and have a first taste of formal verification. Download the file small-example.xml that contains a UPPAAL model of the timed automaton below.
A UPPAAL model consists of several components:
Proc
has two local clocks declared by clock x, y
.P
which is an instance of template Proc
.A concrete simulation corresponds to a run with chosen delays and actions in the automaton. Run a concrete simulation corresponding to the run below:
A (symbolic) simulation corresponds to a path in the zone graph of the automaton depicted below:
bda
as in the run aboves1
In this tutorial, we only consider two kind of properties:
A[] p
which means “In every state of every run, p
holds”.p --> q
meaning “Whenever p
holds, q
eventually holds”.In the menu “Options/Diagnotic Trace” choose “Some”. Select the “Verification” view and check if the following properties hold. Analyse the diagnotic traces provided by UPPAAL if any.
A[] not P.s1
“P is never in state s1”.P.s1 --> P.s0
“Whenever P
is in state s1
, it eventually reaches state s0
”.A deadlock is a configuration from which the only possible evolutions are delay (no transition if feasible, even after some delay). Deadlocks are symptomatic of a bad design. Check if the small example above has deadlocks, by verifying the following property:
A[] not deadlock
“There is no deadlock”In our example, deadlocks correspond to states where, after a long delay, no transition is enabled anymore. Add invariants to locations in order to eliminate all deadlocks (hint: limit possible delays using invariants).
In this second part, we aim at modeling a semaphore that controls the access to a single-track bridge from multiple railways as depicted below.
The semaphore should ensure that no collision occur. The tracks and the semaphores communicates through synchronous messages:
appr
signal when a train is approaching the bridge. The train reaches the bridge within 10 to 20 seconds after the appr
signal has been emitted (unless the train is stopped before)appr
signal, it has up to 10 seconds to send a stop
signal to the train.go
message. Then, the train needs between 7 and 15 seconds to reach the bridge.leave
signal one it has crossed the bridge.A UPPAAL model of the system described above is avalilable in the file train-gate.xml.
appr
, stop
, go
and leave
in the gobal declarations.Train
template is parametrized by a identifier id
that distinguishes the instances of the template. The timed automaton of the Train
implements the protocol above.Semaphore
template implements a mutual exclusion access to the bridge. It (hopefully) stops any train approaching the bridge if an other train is already on the bridge. When a train leaves the bridge, the Semaphore
restarts one of the waiting trains. To that purpose, it stores the set of waiting trains as a set implemented as a vector of booleans. Observe that when appr
is received in state Busy
(i.e. when a train is already crossing the bridge), we need to receive this appr
message and then send a stop
message immediately. We cannot perform more than one communication on a single transition. Hence, the variable stopping_train
is used to remember which train must be stopped. Observe that the state Stopping
is committed as this is a transient state between the two communications.Simulate the following behaviors of the system:
We want to check the following properties:
A[] not deadlock
A[] forall (i : train_id_t) forall (j : train_id_t) (Train(i).Crossing and Train(j).Crossing imply i == j)
Train(1).Approaching --> Train(1).Crossing
From the counter-example returned for the last property, explain why this property does not hold. Suggest a solution to this problem and fix the model. Does it satisfy the 3 properties above? Explain why.
In order to satisfy the liveness property “every approaching train eventually crosses the bridge”, we need a semaphore that implements a fair access policy. The file train-gate-fair.xml replaces the set of waiting trains by a queue. Check that this new model satisfies all the requirements above.
Verify our last model for a growing number of trains. What is the maximal number of trains that can be checked within 60 sec? How long does it take to check for one more train?
The file scheduling.xml contains a UPPAAL model of the job-shop scheduling problem discussed during the talk.
Solution: scheduling-cooloff.xml