Formal Methods in Real-Time Systems (ESSES'03)

A course on formal modeling, specification, and verification of timed systems

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.

Course Material

  1. Concepts, Algorithms, and Tools for Model Checking, by Joost-Pieter Katoen.
  2. 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.
  3. TIMES online help and tutorials.

Other Material

  1. UPPAAL2k: Small Tutorial, by Alexandre David.

Lecturers

The course will be given by Wang Yi and Paul Pettersson.

Outline

  • Oct 1: V262
    • 09.30-10.30, Introduction
    • 10.40-11.45, Modeling and Verifiction of Untimed Systems
    • 12.00-12.15, Demo with UPPAAL
    • 12.00-13.30, Lunch Break
    • 13.30-14.15, Modeling Timed Systems:
      • Timed Automata (.pdf)
      • Modeling Timed Systems: UPPAAL's input languages (.pdf)
    • 14.30-15.20, Verification of Timed Systems:
      • Region Construction
      • Verification of Timed Systems: Symbolic Model-Checking
    • 15.30-16.30, Timed Automata w. Tasks and TIMES,

Recommended Exercises

In addition to attending the lectures, it is recommended that the students solve the following set of exercises.

The exam should be solved using the UPPAAL tool and the TIMES tool. Documentation and installation files can be found at the web sites www.uppaal.com and www.timestool.com.

Last modified: Tue Oct 1 2003 by Paul Pettersson.