Statistical Model Checking for Stochastic Hybrid Systems
Abstract:
Timed automata, priced timed automata and hybrid automata have emerged as useful formalisms for modeling a real-time and energy-aware systems as found in several embedded and cyber-physical systems. Whereas the real-time model checker UPPAAL allows for efficient verification of hard timing constraints of timed automata, model checking of priced timed automata and hybrid automata are in general undecidable -- notable exception being cost-optimal reachability for priced timed automata as supported by the branch UPPAAL Cora.
These obstacles are overcome by UPPAAL-SMC, a new highly scalable engine of UPPAAL, which supports (distributed) statistical model checking of stochastic hybrid systems with respect to weighted metric temporal logic. The talk will review UPPAAL-SMC and (some of) its applications to the domains of energy-harvesting wireless sensor networks, schedulability analysis for mixed criticality systems, as well as smart grids and smart houses. In the talk I will also contemplate on how other branches of UPPAAL may benefit from the new scalable simulation engine of UPPAAL-SMC in order to improve their performance as well as scope in terms of the models that they are supporting. This includes application of UPPAAL-SMC to optimization and refinement checking.