Validation and Performance Analysis of Cyber-Physical Systems


TuToR 2017

2nd Tutorial on Tools for Real-Time Systems

Kim Guldstrand Larsen
CISS, Aalborg University, DENMARK  


Kim G. Larsen: “Validation and Performance Analysis of CPS using UPPAAL” used during tutorial at TuToR 2017

Additional slides

1.     Timed Automata, UPPAAL (1)

2.     Timed Automata, UPPAAL (2)

3.     Priced Timed Automata, UPPAAL CORA

4.     Stochastic Timed Automata, UPPAAL SMC

EXERCISES available here

READINGS (red primary reading)

Frits Vaandrager: A first introduction to UPPAAL

Alexandre David, Kim G Larsen: More features in UPPAAL

Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, Joel Ouaknine, James Worrel: Model Checking Real Time Systems.  To appear in Handbook of Model Checking.

Uli Fahrenberg, Kim G Larsen, Axel Legay: Model-based Verification, Optimization, Synthesis and Performance Analysis of Real-Time Systems.

Johan Bengtsson and Wang Yi: Timed Automata: Semantics, Algorithms and Tools. Concurrency and Petri Nets 2004, LNCS 3098.

Patricia Bouyer, Ulrich Fahrenberg, Kim G. Larsen, Nicolas Markey: Quantitative Modeling and Analysis of Embedded Systems. 

Larsen, Pettersson, Yi: Uppaal in a Nutshell. In Springer International Journal of Software Tools for Technology Transfer, volume 1, issue 1+2, pages 134-152, 1997.

Minimum-Cost Reachability for Priced Timed Automata, Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. In Proceedings of the 4th International Workwhop on Hybrid Systems: Computation and Control 2001.

As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. Kim G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. In Procceedings of the 13th Conference on Computer Aided Verification, (CAV'01). 2001.

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Zheng Wang: Time for Statistical Model Checking of Real-Time Systems. CAV 2011: 349-355.

Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen: Uppaal SMC tutorial. STTT 17(4): 397-415 (2015)

Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Axel Legay, Didier Lime, Mathias Grund Sørensen, Jakob Haahr Taankvist: On Time with Minimal Expected Cost! ATVA 2014

Alexandre David, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis, Jakob Haahr Taankvist: Uppaal Stratego. TACAS 2015: 206-211

Kim G. Larsen, Marius Mikucionis, Marco Muñiz, Jirí Srba, Jakob Haahr Taankvist: Online and Compositional Learning of Controllers with Application to Floor Heating. TACAS 2016

Kim Guldstrand Larsen: Validation, Synthesis and Optimization for Cyber-Physical Systems. TACAS (1) 2017: 3-20