Course Description
The main theme of the course is formal modeling and verification of
real time systems. The goal is to introduce the theories, algorithms
and data structures behind the UPPAAL tool developed
jointly by Uppsala University and Aalborg University.
The course will cover models for finite state systems and
introduction to temporal logics and model checking. The focus will
be put on the theory of timed automata covering the syntax, semantics,
verification problems,
and techniques for symbolic reachability analysis which is the core of
the UPPAAL tool. The practical part of the course will introduce the
UPPAAL modeling and specification languages (the GUI) and the model
checker as well as case studies to show how to use the tool to model
and solve problems.
The course will be given in two days and there will be
a home work, based on UPPAAL for students who plan to take the course
for credits (1p).
Lecturers
The course will be given by
Paul Pettersson
and
Wang Yi.
Schedule
- Day 1, May 17: Vårdnäs
- 12-13 Lunch
- 13-15 Introduction (.pdf),
- 15-16 Demo with UPPAAL
(.pdf)
- 16-17 UPPAAL's modelling and specification language
(.pdf)
- 17-18 Model-Checking Untimed Sytems
(.pdf),
- Day 2, May 18: Vårdnäs
- 8-9 Timed Automata
(.pdf)
- 9-10 Region Construction (slides in the pdf below),
- 10-11 Symbolic Model-Checking
(.pdf),
- 11-12 Timed Automata w. Tasks and TIMES,
(.pdf),
- 12-13 Lunch
|
|
Course Material
- Concepts,
Algorithms, and Tools for Model Checking,
by Joost-Pieter Katoen.
-
UPPAAL
in a Nutshell, by Kim Larsen, Paul Pettersson and
Wang Yi. Springer International Journal of Software Tools for
Technology Transfer, 1(1-2), December 1997, pages 134-152.
Examination
To get the one credit point for the course, the following lab/exam must be solved and handed in. The (firm)
deadline for handing in the exam is set to June 21
2004. Please send your solutions by email to paupet@it.uu.se.
Litterature
- Computation Tree Logics (CTL):
- 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)."
- Timed Systems (Timed Automata, TCTL):
- A
Theory of Timed Automata,
Rajeev Alur and David L. Dill.
Theoretical Computer Science, vol 126, number 2, pages 183-235.
1994.
-
UPPAAL
in a Nutshell, by Kim Larsen, Paul Pettersson and
Wang Yi. Springer International Journal of Software Tools for
Technology Transfer, 1(1-2), December 1997, pages 134-152.
- Timed Automata - Semantics, Algorithms and Tools,
Johan Bengtsson and Wang Yi.
Tutorial on timed automata (a book chapter in Rozenberg et al,
2004, LNCS).
|