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 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.
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.
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
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.
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.
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.
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.