Fifth Summer School on
Formal Techniques
May 17 - May 22, 2015
Menlo College, Atherton,
CA
Material
UPPAAL: modeling,
simulating and verifying real-time systems (using timed automata).
UPPAAL CORA: optimal scheduling and planning (using priced timed
automata).
UPPAAL TRON: on-line conformance
testing of real-time systems (wrt. timed automata).
UPPAAL TIGA: optimal controller
synthesis (using timed game automata).
UPPAAL ECDAR: compositional
design and analysis of real-time systems.
UPPAAL SMC: statistical model
checking for timed automata
UPPAAL STRATEGO: generation and optimization of strategies for
stochastic priced (and hybrid) timed games.
Please download latest versions of UPPAAL and UPPAAL TIGA to your preferred
platform before school. Also download
UPPAAL STRATEGO.
Primary Reading
Frits
Vaandrager: A first introduction to UPPAAL
Alexandre
David, Kim G Larsen: More features in UPPAAL
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.
Alexandre David, Kim G
Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted
Poulsen: UPPAAL SMC Tutorial. To appear in Software Tools
for Technology Transfer.
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.
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, Peter Gjøl Jensen, Kim Guldstrand Larsen, Marius Mikucionis,
Jakob Haahr Taankvist: Uppaal Stratego.
TACAS 2015: 206-211
Efficient
Verification of Real-Time Systems: Compact Data Structure and State-Space
Reduction, Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. In Proceedings
of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco,
California, USA, 3-5 December 1997.
Efficient Timed Reachability Analysis Using Clock Difference
Diagrams. Gerd Behrmann,
Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. In the
proceedings of CAV99, 11th International Conference on Computer-Aided
Verification, July 7-10, 1999, Trento, Italy. Lecture Notes in Computer Science
Volume 1633, Springer-Verlag, 1999.
Clock Difference Diagrams. Kim G. Larsen, Carsten Weise, Wang Yi and Justin Pearson. Nordic Journal of Computing, 1999.
Gerd Behrmann,
Thomas Hune, Frits Vaandrager:
Disitributing Timed Model
Checking -- How the Search Order Matters`, In Proceedings of CAV'2000,
Chicago.
Peter E. Bulychev, Alexandre
David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny
Bøgsted Poulsen: Checking and
Distributing Statistical Model Checking. NASA Formal Methods 2012: 449-463
Andreas Engelbredt Dalsgaard, Alfons Laarman, Kim G. Larsen, Mads Chr. Olesen, Jaco van de Pol: Multi-core Reachability for Timed Automata. FORMATS 2012:
91-106
Alfons Laarman, Mads Chr. Olesen,
Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol: Multi-core Emptiness Checking of Timed Büchi
Automata Using Inclusion Abstraction. CAV 2013: 968-983
UPPAAL - Present and Future. Gerd Behrmann,
Alexandre David, Kim G. Larsen, Oliver Muller, Paul Pettersson, and Wang Yi.
In Proceedings of the 40th IEEE Conference on Decision and
Control (CDC'2001). Orlando, Florida, USA, December 4 to 7, 2001.
UPPAAL
Implementation Secrets: Gerd Behrmann,
Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul
Pettersson, and Wang Yi. In Proceedings of the 7th
International Symposium on Formal Techniques in Real-Time and Fault Tolerant
Systems (FTRTFT'02), 2002.
Gerd Behrmann,
Kim G. Larsen, Radek Pelanek: To Store or
Not to Store, Computer Aided Verification 2003.
Gerd Behrmann,
Patricia Bouyer, Emmanuel Fluery, Kim G Larsen: Static Guard Analysis in Timed Automata Analysis,
TACAS 2003.
Exact Acceleration of Real-Time Model Checking. M. Hendriks and K. G. Larsen. In E. Asarin, O. Maler and
S. Yovine, editors, ENTCS, volume 65 issue 6.
Elsevier Science Publishers, April 2002.
Gerd Behrmann,
Patricia Bouyer, Emmanuel Fleury and Kim G. Larsen. Static Guard
Analysis in Timed Automata Verification.
In Proceedings
of the 9th International Conference on Tools and Algorithms for Construction
and Analysis of Systems (TACAS'03)
Gerd Behrmann,
Patricia Bouyer, Kim G. Larsen and Radek Pelánek.
Lower and Upper Bounds in Zone
Based Abstractions of Timed Automata. In Proceedings of the 10th
International Conference on Tools and Algorithms for Construction and Analysis
of Systems (TACAS'04)
Henrik Ejersbo Jensen, Kim G. Larsen, Arne Skou: Scaling up Uppaal. Formal Techniques in Real-Time and
Fault-Tolerant Systems : 6th International Symposium, FTRTFT
2000 Pune, India.
Kenneth Yrke Jørgensen, Kim
G. Larsen, Jirí Srba: Time-Darts:
A Data Structure for Verification of Closed Timed Automata. SSV 2012:
141-155
Alfons Laarman, Mads Chr. Olesen,
Andreas Engelbredt Dalsgaard, Kim Guldstrand Larsen, Jaco van de Pol: Multi-core
Emptiness Checking of Timed Büchi Automata Using
Inclusion Abstraction. CAV 2013: 968-983
Peter Gjøl Jensen, Kim
Guldstrand Larsen, Jirí Srba, Mathias Grund Sørensen,
Jakob Haahr Taankvist: Memory Efficient Data Structures
for Explicit Verification of Timed Systems. NASA Formal Methods 2014:
307-312
From Timed Automata to Logic - And Back. F. Laroussinie, K.G. Larsen, C.
Weise. In Proc. of MFCS'95
Compositional Model-Checking of Real Time Systems. F. Laroussinie and K.G. Larsen.
In Proc. of CONCUR'95
Beyond Liveness:
Efficient Parameter Synthesis for Time Bounded Liveness
G. Behrmann, K. G. Larsen, J. I. Rasmussen, In proc.
of FORMATS'05, 2005.
Luca Aceto,
Patricia Bouyer, Augusto Burgueño and Kim G.
Larsen. The Power of
Reachability Testing for Timed Automata.
Theoretical Computer Science 300(1-3),
pages 411-475, 2003.
P.R. D'Argenio and J.-P. Katoen and T.C. Ruys and J. Tretmans: The Bounded Retransmission Protocol must be on Time!
Martijn Hendriks: Model
Checking the Time to Reach Agreement
G. Behrmann,
E. Brinksma, M. Hendriks and A. Mader.:
Scheduling
Lacquer Production by Reachability Analysis - A Case Study
Model-Checking
Real-Time Control Programs, Torsten K. Iversen, Kåre J. Kristoffersen, Kim G.
Larsen, Morten Laursen, Rune G. Madsen, Steffen K. Mortensen, Paul Pettersson
and Chris B. Thomasen.
Guided
Synthesis of Control Programs Using UPPAAL, Thomas Hune, Kim G. Larsen, and Paul
Pettersson. In Nordic Journal of Computing (NJC), volume 8, number 1, 2001,
Formal Verification of a TDMA Protocol Start-Up Mechanism, Henrik Lönn and Paul Pettersson.
Formal Design and Analysis of a Gear Controller, Magnus Lindahl, Paul Pettersson and
Wang Yi. In Proceedings of the 4th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems
Leslie Lamport:
Real-Time
Model Checking is Really Simple (Leader Election in Mobile Ad Hoc
Networks), CHARME 2005.
Juhan Ernits. Memory Arbiter Synthesis and
Verification for a Radar Memory Interface Card. Nordic Journal of Computing, 12(2):68-88.
Testing
Real-time Embedded Software using Uppaal-TRON - An Industrial Case Study.
Kim G. Larsen, Marius Mikucionis, Brian Nielsen, Arne Skou. The 5th ACM International
Conference on Embedded Software. Jersey
City, NJ, USA. September 18-22, 2005.
Alexandre David, Jacob Illum, Kim G.
Larsen, Arne Skou: Model-based
Framework for Schedulability Analysis Using Uppaal 4.1
Optimal
Scheduling Using Priced Timed Automata G. Behrmann,
K. G. Larsen, J. I. Rasmussen, ACM SIGMETRICS Performance Evaluation Review,
vol. 32, nb. 4, 2005, pp.
34-40, ACM Press.
Optimal Conditional
Reachability of Multi-Priced Timed Automata K. G. Larsen, J. I. Rasmussen,
In proc. of FOSSACS'05, pp. 234-249, Springer Verlag,
2005.
Priced Timed
Automata: Decidability Results, Algorithms, and Applications G. Behrmann, K. G. Larsen, J. I. Rasmussen, In proc. of
FMCO'04, LNCS vol. 3657, pp. 162-186, Springer Verlag,
2005.
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. LNCS 2102,
pages 493-505, G. Berry, H. Comon, A. Finkel (Eds.). Paris, France, July 18 to 23, 2001.
Guided Synthesis of Control Programs Using UPPAAL. Thomas Hune,
Kim G. Larsen and Paul Pettersson. In Proceedings of the IEEE ICDCS
International Workshop on Distributed Systems Verification and Validation ( DSVV'2000), pages E15-E22, Ten H. Lai (Ed.). Taipei,
Taiwan, April 10-13, 2000.
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 (HSCC'01). Rome, Italy, March 28 to 30,
2001. LNCS 2034, pages 147-161, Maria Domenica Di
Benedetto and Alberto Sangiovanni-Vincentelli (Eds.)
Efficient
Guiding Towards Cost-Optimality in UPPAAL. Gerd Behrmann,
Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. In Proceedings of the 7th
International Conference on Tools and Algorithms for the Construction and
Analysis of Systems (TACAS'01). Genova, Italy,
April 2 to 6, 2001. LNCS 2031, pages 174-188, T. Margaria
and W. Yi (Eds.).
Guided Synthesis of Control Programs Using UPPAAL. Thomas Hune, Kim G. Larsen, and Paul
Pettersson. In Nordic Journal of Computing (NJC), volume 8, number 1,
2001, pages 43-64
Efficient
Guiding Towards Cost-Optimality in UPPAAL, Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G.
Larsen, Paul Pettersson, and Judi Romijn. In Proceedings of the 7th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems (TACAS'01).
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 (HSCC'01).
Kim Guldstrand Larsen, Jacob Illum Rasmussen: 2005 in: Proceedings of Foundations of
Software Science and Computation Structures
Optimal Conditional Reachability for Multi-Priced Timed Automata
Patricia
Bouyer, Ed Brinksma and Kim G. Larsen. Staying
Alive As Cheaply As Possible. In Proceedings of the 7th
International Conference on Hybrid Systems: Computation and Control (HSCC'04),
Philadelphia, Pennsylvania, USA, March 2004, LNCS 2993
Resource-Optimal
Scheduling Using Priced Timed Automata J. I. Rasmussen, K. G. Larsen, K.
Subramani, In proc. of TACAS'04, pp. 220-235, Springer Verlag,
2004.
G. Behrmann, E. Brinksma, M. Hendriks and A. Mader.: Scheduling Lacquer Production by Reachability Analysis - A
Case Study
Franck Cassez,
Kim Guldstrand Larsen: The Impressive Power of
Stopwatches. CONCUR 2000: 138-152
Gerd Behrmann,
Agnes Cougnard, Alexandre David, Emmanuel Fleury, Kim
G. Larsen, and Didier Lime: UPPAAL-Tiga: Time for Playing Games! CAV
2007, LNCS 4590.
Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen,
and Didier Lime. Efficient
on-the-fly algorithms for the analysis of timed games. In Martín Abadi and Luca de Alfaro, editors, Proceedings of the 16th International
Conference on Concurrency Theory (CONCUR'05), volume 3653 of Lecture Notes in Computer Science,
pages 66-80, San Francisco, CA, USA, August 2005. Springer.
Copyright Springer-Verlag.
Patricia Bouyer, Franck Cassez, Emmanuel
Fleury and Kim G. Larsen. Synthesis
of Optimal Strategies Using HyTech. In Proceedings of the
Workshop on Games in Design and Verification (GDV'04), Boston, Massachusetts,
USA, July 2004, ENTCS 119(1), pages 11-31.
Patricia
Bouyer, Franck Cassez, Emmanuel Fleury and
Kim G. Larsen.
Optimal
Strategies in Priced Timed Game Automata.
In Proceedings
of the 24th Conference on Fundations of Software
Technology and Theoretical Computer Science (FSTTCS'04), Chennai, India,
December 2004, LNCS 3328, pages 148-160.
T-UPPAAL: Online Model-based Testing of Real-time Systems,
tool demo. Marius Mikucionis, Kim G. Larsen, Brian Nielsen. 19th IEEE
International Conference on Automated Software Engineering, 396-397. Linz, Austria.
September 24, 2004.
Online
Testing of Real-time Systems Using Uppaal. Kim G. Larsen, Marius Mikucionis, Brian Nielsen. Formal Approaches
to Testing of Software. Linz, Austria.
September 21, 2004.
Time-Optimal
Real-Time Test Case Generation using UPPAAL. Anders Hessel,
Kim G. Larsen, Brian Nielsen, Paul Pettersson, and Arne Skou. In Proceedings of
the 3rd International Workshop on Formal Approaches to Testing of
Software (FATES'03), 2003.
Testing
Real-time Embedded Software using Uppaal-TRON - An Industrial Case Study.
Kim G. Larsen, Marius Mikucionis, Brian Nielsen, Arne Skou. The 5th ACM International
Conference on Embedded Software. Jersey
City, NJ, USA. September 18-22, 2005.
Alexandre David, Dehui Du,
Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted
Poulsen, Sean Sedwards: Statistical Model Checking for
Stochastic Hybrid Systems. HSB 2012: 122-136
Alexandre David, Dehui Du,
Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis:Optimizing Control Strategy
Using Statistical Model Checking. NASA Formal Methods 2013: 352-367
Alexandre David, Kim G.
Larsen, Axel Legay, Danny Bøgsted Poulsen: Statistical Model Checking of Dynamic Networks of Stochastic
Hybrid Automata. ECEASST 66 (2013)
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: 129-145