Slides
Kim G. Larsen: “Validation and Performance
Analysis of CPS using UPPAAL” used during tutorial at TuToR 2017
Additional slides
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