Validation and Performance Analysis of Cyber-Physical Systems in UPPAAL
Timed automata, priced timed automata as well as stochastic timed automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. During several years the real-time model checker UPPAAL has been developed allowing for efficient verification of hard timing constraints of timed automata.
Moreover a number of significant branches now exists providing new functionality, e.g. UPPAAL CORA which offers efficient support for optimization and the recent branch UPPAAL SMC which offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata. The lecture will review and give on-line and hands-on demonstration of the various branches of UPPAAL and indicate their concerted applications to a range of real-time and energy-centric e.g. schedulability analysis of multi-core and mixed-criticality systems, WCET analysis, performance analysis of MAC and routing protocols for mesh-networks, mission optimization of battery-aware nano-satellites.
Installation Instructions
Please go to www.uppaal.org and download the development version 4.1.19 (this includes both classical UPPAAL and UPPAAL SMC).
