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!

Examples:
 

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)
 

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    

 

 

 

 

Home

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.

Dismiss