Symbolic and Statistical Model-Checking in UPPAAL

Kim Larsen / PERSYVAL-Lab

In these two talks we will cover the theory of timed automata, our fundamental modeling language underlying the verification tool UPPAAL.  Also, a number of extensions of this formalisms will be presented including timed games, priced timed automata and games, energy automata games, stochastic extensions of these as well as the most recently very expressive formalism of stochastic hybrid automata, which is particularly well-suited for modeling cyber-physical systems.  We will review a number of associated decision problems related to model-checking, refinement checking and optimal scheduling and synthesis for these models that are highly relevant for cyber-physical systems.

The lectures will also emphasize the substantial research effort in the design of algorithms and datastructures for efficient analysis of timed automata and its extensions as to be found in the verification tool UPPAAL and its various branches.  Also, substantial focus will be on the most recent statistical model checking engine of UPPAAL, where properties are settled up to user-specified level of confidence based on randomly generated simulation runs.

The lectures will include ample demonstration of UPPAAL and it extensions, in particular UPPAAL SMC, as well as applications to a range of real-time and cyber-physical examples including schedulability and performance evaluation of mixed criticality systems, modeling and analysis of biological systems, energy-aware wireless sensor networks, smart grid and energy aware buildings and battery scheduling.