Welcome!

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.

Tutorial

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.