Modeling and Verification of Concurrent Real-Time Systems

Feb. 12 - 16, 2007, Department of Information and Communication Technology, University of Trento

Results

  • Students who completed the assignments and the project

    OBS:

    To get 3 credits for the course, you must send your solutions for the assignments listed below and a report for either the project described below or a project from your own research. The deadline is May 1, 2007.

    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 covers:
    • Transition systems and Temporal Logics
    • Finite-state systems: SPIN and Promela
    • Infinite state systems: decidability and algorithms
    • Theory of timed systems: timed automata and decision problems
    • UPPAAL: input languages, algorithms and data structures (DBM)
    • TIMES: from models to code guaranteeing timing constraints

    Lecturers

    Bengt Jonsson och Wang Yi, Uppsala University, Sweden.

    Schedule and Lecture Notes

    Tools

    Literature and references

    • Model-checking of untimed systems
    • 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