Verification, Optimization, Performance Analysis and Synthesis of Cyber-Physical Systems

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. In this talk we will survey how the various components of the UPPAAL tool-suite over a 20 year period have been developed to support various analysis of these formalisms. This includes the classical usage of UPPAAL as an efficient model checker of hard real time constraints of timed automata models, but also the branch UPPAAL CORA which has been extensively used to find optimal solutions to time-constrained scheduling problems. More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies - and subsequent executable control programs - for safety and reachability objectives. More recently the branch UPPAAL SMC offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata, and the branch UPPAAL STRATEGO supports synthesis (using machine learning) of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and highlight their concerted applications to a selection of real-time and cyber-physical examples.