Statistical Model Checking of Stochastic Hybrid Systems using UPPAAL-SMC

Kim Guldstrand Larsen / Persyval-Lab

Timed automata, priced timed automata and energy 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 energy 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, the new highly scalable engine of UPPAAL, which supports (distributed) statistical model checking of stochastic hybrid systems with respect to weighted metric temporal logic.

The lecture will review UPPAAL-SMC and its applications to a range of  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 grids and energy aware buildings and battery scheduling.  Also, we shall see 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 counter example generation, refinement checking, controller synthesis, optimization, testing and meta-analysis.

Kim Guldstrand Larsen is a full professor in computer science and director of the centre of embedded software systems (CISS). He received his Ph.D from Edinburgh University (Computer Science) 1986, is an honorary Doctor (Honoris causa) at Uppsala University 1999 and at Normal Superieure De Cachan, Paris 2007. He has also been an Industrial Professor in the Formal Methods and Tools Group, Twente University, The Netherlands. His research interests include modeling, verification, performance analysis of real-time and embedded systems with application and contributions to concurrency theory and model checking. In particular since 1995 he has been prime investigator of the tool UPPAAL and co-founder of the company UP4ALL International. He has published more than 230 publications in international journals and conferences as well as co-authored 6 software-tools, and is involved in a number of Danish and European projects on embedded and real-time systems. His H-index (according to Harzing's publish or perish, January 2012) is 63  (the highest in Denmark. He is life-long member of the Royal Danish Academy of Sciences and Letters, Copenhagen, and is member of the Danish Academy of Technical Sciences as well as member of Acedemia Europeae. Since January 2008 he has been member of the board of the Danish Independent Research Councils, as well as Danish National Expert for the European ICT-program.