UPPAAL provides a tool-suite supporting model checking, performance analysis, testing, synthesis and learning for real-time systems. Based on the underlying modeling formalism of timed automata, significant effort has been put into development and implementation of efficient datastructures and algorithmic methods. By now these methods have resulted in a variety of symbolic, statistical and randomized engines.

In the talk I will present the three algorithmic methods and highlight their particular benefits individually and in combinations. This include: 1) Randomized methods are useful in early phases of development for fast discovery leaving the use of expensive symbolic verification to the end of development. 2) Combining randomized and statistical methods we have proposed a new falsification testing methodology that is aware of expected system usage and underlying risks associated with different faulty behaviors, allowing for a ranking of counterexamples based on their expected impact. 3) UPPAAL Stratego combines symbolic and statistical (learning) methods for constructing safe and near-optimal control strategies.

We shall also report on current effort made towards a hierarchical modelling formalism, where first prototypes are being obtained using model transformations to the existing non-hierarchical formalism.

Finally during the talk we will provide on-line demo of the new release UPPAAL 5.0.