Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.). The tool is developed in collaboration between the Department of Information Technology at Uppsala University, Sweden and the Department of Computer Science at Aalborg University in Denmark. We proposed tutorial at RTSS'05 aims at teaching how to use Uppaal with all its advanced features.
The tutorial aims at introducing timed automata as a language for modeling and analyzing timed systems. It is graphical language that can be easily learnt with the intuitive graphical interface of UPPAAL. The tutorial is based on examples from various areas, including embedded systems, real-time scheduling, communication protocols, etc. Participants of the tutorial are shown how to model in UPPAAL, using all the expressive power of the implemented extension of timed automata. We demonstrate how to best utilize features of the tool, how to avoid certain pitfalls, and how to specify and check properties written in a subset of TCTL.
The different topics that are addressed are modeling, analyzing, synthesizing, and testing real-time systems using our verification tool UPPAAL and its recent extensions towards scheduling, optimal planing, and testing. UPPAAL is derived in different specialized flavours (Cora, Tron, TiGa, Times) to tackle these different problems.
Apart from applications, the tutorial provides insights into the underlying formalisms for modeling and specification, as well as how to most efficiently exploit the algorithms and data structures in the tools.
Latest NewsWeb page for the tutorial
25 Oct 2005
UPPAAL @ RTSS'05 has a shiny new web page.Major update
2 Dec 2005
Litterature and the program have been completed.
The modeling language of UPPAAL 3.4 (and 3.5) is backward compatible and will remain so. It is an extension of timed automata language with integers and arrays (of channels and integers). The development version (3.5) offers a rich subset of C/C++ with function calls, loops, and call by reference. This allows the user to design compact models.
The technology behind UPPAAL is mature and has been constantly improved since the first release of UPPAAL in 1995. Advanced algorithms (such as symmetry reduction (3.5), minimal graph representation, bitstate hashing) and optimized memory management keep the tool competitive on large scale models. A distributed version of the tool can also be deployed harness the power of clusters.
UPPAAL is based on the latest internal development version of UPPAAL, containing the latest performance and language improvements. It implements state-of-the-art algorithms in model-checking of timed automata.