Keynote Speaker: Kim G. Larsen, Aalborg University
From Testing and Verification to Performance Analysis and Synthesis of Cyber-Physical Systems
Tuesday 5 July 2016, 1st session after lunch
Abstract
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 component of the UPPAAL tool-suite over a 20 year period has been developed to support various type of 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 TRON which have been extensively used to perform on- and off-line conformance testing of real-time systems with respect to timed automata specifications.
More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies – and subsequent executable control programs – for safety and reachability objectives. Most 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) and evaluation of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and indicate their concerted applications to a range of real-time and cyber-physical examples.
CV
Kim G. Larsen is a professor in the Department of Computer Science at Aalborg University within the Distributed and Embedded Systems Unit and director of the ICT-competence center CISS, Center for Embedded Software Systems. In 2015, he won an ERC Advanced Grant with the project LASSO for learning, analysis, synthesis and optimization of cyber physical systems. He is also director of the Sino-Danish Basic Research Center IDEA4CPS, the Danish Innovation Network InfinIT, as well as the newly founded innovation research center DiCyPS: Data Intensive Cyber Physical Systems. Kim G Larsen is prime investigator of the tool UPPAAL and co-founder of the company UP4ALL International. In 2013 he was the recipient of the CAV Award for his work on UPPAAL as "the foremost model checker for real-time Systems". Kim G Larsen became Honorary Doctor (Honoris causa) at Uppsala University, Sweden, in 1999. In 2007 he became Knight of the Order of the Dannebrog. In 2007 he became Honorary Doctor (Honoris causa) at ENS Cachan, France. In 2012 he became Honary Member of Academia Europaea. Since 2016 he has been appointed INRIA International Chair for a 5 year period.