UFIT (Uppaal Fault Injector for Timed automata): A Tool for Modeling Faults in UPPAAL Timed Automata

UFIT is a tool for modeling five types of faults, namely, message loss, transient, byzantine, stuck-at, and fail-stop faults in UPPAAL timed automata models. Given the fault-free timed automata model and the selection of a type of fault, UFIT models the faults and generates the fault-affected timed automata model automatically. As a result, the designer can analyze the fault-affected model to see how the model behaves in the presence of faults.

For downloading UFIT, please click here!


1) The Fischer's mutual exclusion protocol
Fischer's protocol is designed to ensure mutual exclusion among several processes (5 processes here) competing for a critical section using timing constraints and a shared variable id. In each process P, the process goes to a request location req if it is the turn for no process to enter the critical section (id==0). After x time units in req (0 <= x <= k), P goes to the wait location and sets id to its process ID. Finally, after at least k time units, P enters the critical section cs if it is its turn. The Fischer's protocol satisfies the following set of requirements/properties in the absence of faults:

SPEC 1: A[] not deadlock
SPEC 2: P(i).req --> P(i).wait
SPEC 3: A[] P1.cs + P2.cs + P3.cs + P4.cs + P5.cs <=1

2) The train-gate problem

The train gate problem is a railway control system which controls access to a bridge for several trains. The bridge is a critical shared resource that may be accessed only by one train at a time. The system is defined as a number of trains and a controller.
There are timing constraints on the trains before entering the bridge. When approaching, a train sends a appr! signal. Thereafter, it has 10 time units to receive a stop signal. This allows it to stop safely before the bridge. After these 10 time units, it takes further 10 time units to reach the bridge if the train is not stopped. If a train is stopped, it resumes its course when the controller sends a go! signal to it after a previous train has left the bridge and sent a leave! signal. The model satisfies the following properties in the absence of faults:

SPEC 1: A[] not deadlock
SPEC 2: E<> Train(0).Cross and (forall (i : id_t) i != 0 imply Train(i).Stop)
SPEC 3: A[] forall (i : id_t) forall (j : id_t)
Train(i).Cross && Train(j).Cross imply i == j
SPEC 4: Train(0).Appr --> Train(0).Cross

3) The Vikings problem

In the Vikings problem, four Vikings want to cross a bridge at night, but they have only one torch and the bridge can only carry two of them. Thus, they can only cross the bridge in pairs and one has to bring the torch back to the other side before the next pair can cross. Each Viking has different speed. The question is whether it is possible that all the Vikings cross the bridge within a certain time. This example is comparable to the question if a packet can reach its receiver in a given time limit in a communication network/Network on Chip (NoC) system. The TA model satisfies the following properties in the absence of faults:

SPEC 1: A[] not deadlock
SPEC 2: E<> Viking1.safe
SPEC 3: E<> Viking1.safe and Viking2.safe and Viking3.safe and Viking4.safe

The following models are obtained using UFIT automatically. We have played with the output models to show them more clearly though!

Fischer's mutual exclusion protocol

Fault-free model   Transient faults   Fail-stop faults
Byzantine faults   Stuck-at faults    

Train-Gate protocol

Fault-free model   Fail-stop faults   Message faults
Fault-free model   Fail-stop faults   Message faults

The Vikings problem

Fault free model   Message loss faults   Fail-stop faults
Fault free model   Message loss faults   Fail-stop faults
Transient faults   Byzantine faults   Stuck-at 1 faults




More Examples!



Andrew File System Retirement

Andrew File System, which hosts this address, will be ending service by January 1, 2021. Learn about the retirement process, managing your existing files, and alternative services at the Andrew File System Retirement Information Page.