Real Time Systems
Verification, Performance Analysis, and Controller Synthesis  

using UPPAAL 

Kim Guldstrand Larsen
CISS, Aalborg University, DENMARK  

Shanghai / Beijing – July, 2009
 

Material

  1. Tools
     
  2. General Reading
  3. Efficient Datastructures
  4. Distributed Model Checking
  5. Other Efficient Techniques
  6. Logic and Preorders
  7. Applications
     
  8. Planning and Scheduling
  9. Hybrid Systems
  10. Timed Games
  11. Testing
     

 

 

Tools

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 priced timed game automata).

UPPAAL ECDAR: compositional design and analysis of real-time systems.

UPPAAL SMC: statistical model checking for timed automata

Have a look at web-pages of the above tools - ideally try to download UPPAAL and play with it.

General Reading

Various: Quasimodo Industrial Handbook on Quantitative Modeling and Analysis for Embedded Systems (draft, to be published by Springer)

Aceto, Ingolfsdottir, Larsen, Srba: Reactive Systems: Modelling, Specification and Verification.  Cambridge University Press (Part II: A theory of real time systems).

Uppaal pamphlet brief introduction to UPPAAL  on two pages.

Behrmann, David, Larsen: A Tutorial on Uppaal

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

Ulrich Fahrenberg, Kim G. Larsen, Claus Thrane:   Verification, Performance Analysis and Controller Synthesis for Real-Time Systems. Marktoberdorf 2008 Lecture Notes. NATO ASI series, IOS Press Publishers, 2009

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

Alexandre David, Jacob Illum, Kim G. Larsen, Arne Skou: Model-based Framework for Schedulability Analysis Using Uppaal 4.1

 

Joost-Pieter Katoen: Concepts, Algorithms, and Tools for Model Checking (Especially Chapter 4)

Rajeev Alur: Timed Automata (survey) NATO-ASI 1998 Summer School on Verification of Digital and Hybrid 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.

Alexandre David: UPPAAL2k: Small Tutorial

 

Efficient Data Structures

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.

 

Distributed Modelchecking

Gerd Behrmann, Thomas Hune, Frits Vaandrager: Disitributing Timed Model Checking -- How the Search Order Matters`, In Proceedings of CAV'2000, Chicago.

 

Other Efficient Techniques

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.

 

Logic and Preorders

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.

 

Applications

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.

 

 

Planning and Scheduling

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

 

Hybrid Systems

Franck Cassez, Kim Guldstrand Larsen: The Impressive Power of Stopwatches. CONCUR 2000: 138-152

 

Timed Games

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.

 

Testing

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.