Introduction to formal verification with UPPAAL

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

Starting with a small example

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.

small example

A UPPAAL model consists of several components:

Simulation

A concrete simulation corresponds to a run with chosen delays and actions in the automaton. Run a concrete simulation corresponding to the run below:

run

A (symbolic) simulation corresponds to a path in the zone graph of the automaton depicted below:

zone graph

Verification

In this tutorial, we only consider two kind of properties:

illustration of properties

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.

Deadlocks

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:

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).

Train crossing

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.

Train gate picture

The semaphore should ensure that no collision occur. The tracks and the semaphores communicates through synchronous messages:

A UPPAAL model of the system described above is avalilable in the file train-gate.xml.

Simulation

Simulate the following behaviors of the system:

Verification

We want to check the following properties:

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.

Fair semaphore

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.

Complexity of model-checking in practice

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?

Scheduling (exercise)

The file scheduling.xml contains a UPPAAL model of the job-shop scheduling problem discussed during the talk.

Solution: scheduling-cooloff.xml