Modeling and Verification of Timed Systems

May 7-8, 2012, CUGS, Linköping University.

OBS:

To get 1.5 ECTS credits for the course, you must send your solutions (to Wang) for the assignments listed below. The deadline is June 7, 2012.

Course Description

The main goal of this course is to introduce the theories, algorithms and data structures behind model-checking tools in particular the UPPAAL tool for timed systems, developed jointly by Uppsala University and Aalborg University. The topics cover:
  • Transition systems, CTL and basic model checking algorithms
  • Theory of timed systems: timed automata, decision problems, TCTL
  • UPPAAL: input languages, algorithms and data structures (DBM)
  • Resource modeling and schedulability analysis

Lecturer

Wang Yi, Uppsala University, Sweden.

Schedule and Lecture Notes

Tools

Literature and references

  • Temproal Logics (LTL, CTL):
    • An Automata-Theoretic Approach to Automatic Program Verification, Moshe Y. Vardi, Pierre Wolper. LICS 1986: 332-344. Also as "Reasoning About Infinite Computations. Inf. Comput. 115(1): 1-37 (1994)"
    • 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):
  • Tools (UPPAAL, TIMES):

Assignments