From Pre-Verification and -Analysis to Post-Synthesis and -Optimization for Timed and Hybrid Systems

Kim G. Larsen
Aalborg University, Denmark


Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. Within the last 20 years the various components of the UPPAAL tool-suite has been developed to support various types of analysis of these formalisms.

This includes the classical usage of UPPAAL offering efficient pre-deployment model checking of hard real time constraints of timed automata models. More recently the branch UPPAAL offers a highly scalable statistical model checking engine supporting both pre- and post-deployment performance analysis of stochastic hybrid automata.

The newest branch UPPAAL STRATEGO supports synthesis (using machine learning) and evaluation of near-optimal yet safe strategies for stochastic hybrid games. Whereas originally conceived to be used prior to deployment new industrial applications within home automation have been using STRAGEGO during deployment to perform on-line synthesis.