Getting Ready For The Tutorial

Before coming to the tutorial, please check your installation of Java. You need Java 1.5 installed on your machine under Windows or Linux. Please refer to the Java homepage to download appropriate software.
It is a good idea to download Uppaal (latest 3.6 alpha version) prior to the tutorial even though you will be given a CD with the distribution. The tool is free for non commercial purpose and can be downloaded from our homepage.
You are welcome to browse the available documentation (papers, help, tutorials, FAQ) on the Uppaal homepage under "documentation" if you are impatient to discover the tool. This may help you prepare questions for the tutorial.

Schedule

9:00 - 10:30	Session 1: Introduction to Uppaal.
10:30 - 11:00	Coffee Break.
11:00 - 12:00	Session 2: Inside Uppaal - Basics.
12:00 - 13:30	Lunch.
13:30 - 15:00	Session 3: Inside Uppaal - Advanced.
15:00 - 15:30	Coffee Break.
15:30 - 17:00	Session 4: Beyond Uppaal.
19:00 - 21:00	RTSS'05 Welcome Reception.

Sessions

Session 1: Introduction to Uppaal.

Presentation of the tool, model-checking, tool architecture. Timed automata in Uppaal, semantics, query language, zones and operations on zones. Slides Demo, guided exercises. Slides.

Session 2: Inside Uppaal - Basics.

Data structures, reachability algorithm, liveness algorithm, deadlock. Slides

Session 3: Inside Uppaal - Advanced.

Model-checker architecture, reachability & liveness pipeline, virtual machine, sharing, minimal graph, to store or not to store, symmetry. Slides.
Practice on modeling patterns, exercises. Slides.

Session 4: Beyond Uppaal.

Uppaal Cora, Tron, Tiga. Open source components (DBM library, libutap, parts of the GUI). Slides.
Times. Slides. Cover. Slides.
Exercises if time left.

Material

• Uppaal pamphlet: brief introduction to Uppaal on two pages.
• A Tutorial on Uppaal: the current updated tutorial on Uppaal.
• [by04] Johan Bengtsson and Wang Yi. Timed Automata: Semantics, Algorithms and Tools. Concurrency and Petri Nets 2004, LNCS 3098.
• Concepts, Algorithms, and Tools for Model Checking (chapter 4), by Joost-Pieter Katoen.
• Automata For Modeling Real-Time Systems. ICALP 1990, pages 322-335. Also as "A Theory of Timed Automata, Rajeev Alur and David L. Dill. Theoretical Computer Science, vol 126, number 2, pages 183-235. 1994".
• Times online help and tutorials.

Litterature

General Reading

• Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach, Edmund M. Clarke, E. Allen Emerson, A. Prasad Sistla. POPL 1983: 117-126. Also as "Automatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications. ACM Trans. Program. Lang. Syst. 8(2): 244-263 (1986)."
• An Automata-Theoretic Approach to Automatic Program Verification, Moshe Y. Vardi, Pierre Wolper. (Preliminary Report). LICS 1986: 332-344. Also as "Reasoning About Infinite Computations. Inf. Comput. 115(1): 1-37 (1994)".
• [dill89] David L. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. LNCS 407. Springer Berlin 1989, pp 197-212.
• [lpw:fct95] Kim G. Larsen, Paul Pettersson, and Wang Yi. Model-Checking for Real-Time Systems. Fundamentals of Computation Theory 1995, LNCS 965 pages 62-88.
• [lpy97] Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer , October 1997, number 1-2 pages 134-152.
• [alur98] Rajeev Alur. Timed Automata (survey). NATO-ASI 1998 Summer School on Verification of Digital and Hybrid Systems.
• [bdl04] Gerd Behrmann, Alexandre David, and Kim G. Larsen. A Tutorial on UPPAAL. 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04), LNCS 3185.

Efficient Data Structures

• [rokicki93] Tomas Gerhard Rokicki. Representing and Modeling Digital Circuits. Ph.D. thesis, Standford University 1993.
• [llpw97] Kim G. Larsen, Fredrik Larsson, Paul Pettersson and Wang Yi. Efficient Verification of Real-Time Systems: Compact Data Structure and State-Space Reduction. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 14-24. San Francisco, California, USA, 3-5 December 1997.
• [blpww99] Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient Timed Reachability Analysis Using Clock Difference Diagrams. 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.
• [lwwp99] Kim G. Larsen, Carsten Weise, Wang Yi and Justin Pearson. Clock Difference Diagrams. Nordic Journal of Computing, 1999.
• [bengtsson02] Johan Bengtsson. Clocks, DBM, and States in Timed Systems. Ph.D. thesis, Uppsala University 2002.

Distributed Model-Checking

• [bhv00] Gerd Behrmann, Thomas Hune, Frits Vaandrager. Distributing Timed Model Checking -- How the Search Order Matters. In Proceedings of CAV'2000, Chicago.

Other Efficient Techniques

• [bdlmpw01] Gerd Behrmann, Alexandre David, Kim G. Larsen, Oliver Muller, Paul Pettersson, and Wang Yi. UPPAAL - Present and Future. In Proceedings of the 40th IEEE Conference on Decision and Control (CDC'2001). Orlando, Florida, USA, December 4 to 7, 2001.
• [bbdlpw02]Gerd Behrmann, Johan Bengtsson, Alexandre David, Kim G. Larsen, Paul Pettersson, and Wang Yi. UPPAAL Implementation Secrets. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT'02), 2002.
• [hl02] M. Hendriks and K. G. Larsen. Exact Acceleration of Real-Time Model Checking. In E. Asarin, O. Maler and S. Yovine, editors, ENTCS, volume 65 issue 6. Elsevier Science Publishers, April 2002.
• [blp03] Gerd Behrmann, Kim G. Larsen, Radek Pelanek. To Store or Not to Store. Computer Aided Verification 2003.
• [bbfl03] Gerd Behrmann, Patricia Bouyer, Emmanuel Fleury, Kim G Larsen. Static Guard Analysis in Timed Automata Analysis. TACAS 2003.

Planning and Scheduling

• [hlp00] Thomas Hune, Kim G. Larsen and Paul Pettersson. Guided Synthesis of Control Programs Using UPPAAL. 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.
• [hscc01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. 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.)
• [tacas01] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, and Judi Romijn. Efficient Guiding Towards Cost-Optimality in UPPAAL. 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.).
• [cav01] Kim G. Larsen, Gerd Behrmann, Ed Brinksma, Ansgar Fehnker, Thomas Hune, Paul Pettersson, and Judi Romijn. As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. 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.
• [hlp01] Thomas Hune, Kim G. Larsen, and Paul Pettersson. Guided Synthesis of Control Programs Using UPPAAL. In Nordic Journal of Computing (NJC), volume 8, number 1, 2001, pages 43-64.

Hybrid Systems

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

Logic and Pre-orders

• [llw95] F. Laroussinie, K.G. Larsen, C. Weise. From Timed Automata to Logic - And Back. In Proc. of MFCS'95.
• [ll95] F. Laroussinie and K.G. Larsen. Compositional Model-Checking of Real Time Systems. In Proc. of CONCUR'95.