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<> and and and


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)

3) Producer-Consumer Protocol using Loosely-Timed Coding Style


4) Memory-Mapped Buses Program using Approximately-Timed Coding Style


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    






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.