USlicer: A Tool for Model Slicing UPPAAL Timed Automata Models
USlicer is a tool for slicing timed automata models. Given a timed automata model and a property of interest, USlicer generates a sliced version of the model for verifying the property of interest. As a result, the designer can analyze the sliced version in less time and memory.
For downloading USlicer, please click here!
1) The Vikings problem
This example is slightly different from that in the literature since
we want to make the model a little bit more complex as an input to
USlicer. 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. Also, we track the
number of times the bridge is utilized using a global variable (the
variable "a"). 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 property:
Phi: E<> Viking1.safe and Viking2.safe and Viking3.safe and Viking4.safe
2) The Alternating Bit Protocol
This example provides reliable communication over a network service
that sometimes looses messages. This protocol uses a one-bit sequence
number (which alternates between 0 and 1) in each message and an
acknowledgment to determine whether the message must be retransmitted.
The system consists of three automata running in parallel, Sender,
Receiver and Faulty Buffer, as shown below. The task of Sender is to
transmit portions of data, which represents some computations performed
in real systems. In our example they are succeeding numbers modulo N.
Sender sends each portion accompanied with the bit to Faulty Buffer.
Then it waits for an acknowledgment. If the value of the acknowledgment
is the same as the value of the bit, then the message is treated as
delivered and the value of the bit flips. Otherwise the message is
retransmitted. The message is also retransmitted, if no acknowledgment
comes within T units of time (the timeout is modeled by the clock x).
Receiver waits until it gets the message from Faulty Buffer, then it
acknowledges receipt of the message and compares its sequence number
with the bit value. If they are equal, it changes the value of the bit
and accepts the message. Otherwise it waits for another message. Faulty
Buffer accepts a message from Sender or an acknowledgment from Receiver
and forwards it respectively or looses it. The clock y is used to model
transmission delays, which are between d and D units of time.
Phi: A (Sender.snd_init --> s_bit == r_bit)
The following models are the original model and the sliced model generated by USlicer.
The Vikings problem
|The original viking automaton||The torch automaton|
|The revised viking automaton||The sliced viking automaton|
The Alternating Bit Protocol
|The Sender automaton||The Receiver automaton|
|The Buffer automaton|
The sliced Sender automaton
|The sliced Buffer automaton|