Estonian Winter Schools in Computer Science    
Eesti arvutiteaduse talvekoolid
EWSCS 2001
EATTK 2001

Prof. Kim G. Larsen

Department of Computer Science
Aalborg University, Denmark

Tool Supported Validation of Real-Time and Hybrid Systems


In 1989, Rajeev Alur and David Dill introduced the notion of timed automata together with some basic decidability (and undecidability) results. Since then, this formalism and its hybrid extensions have proved extremely useful in modeling real-time and hybrid behaviour, while allowing for efficient automatic analysis of real-time temporal properties. In this course we aim at familiarizing the audience with the basic ideas of these models, the associated real-time logics, and the fundamental techniques underlying a number of associated decidability results.

The first theoretical decidability results was based on the so-called region technique. Since then a number of tools for automatic verification of real-time and hybrid systems has emerged (e.g. UPPAAL and HyTech). These tools have been successfully applied in a number of industrial case studies, and their implementations are based on a variety of newly developed, efficient data structures and algorithms for symbolic representation and manipulation of the state-space of real-time and hybrid systems. In the course, we will offer a detailed explanation to the most promising of these techniques. Also, we shall provide on-line demonstration of the tool UPPAAL and show how it can be used to analyse real-time systems implemented in LEGO MindStorm.


            Joost-Pieter Katoen: Concepts, Algorithms, and Tools for Model Checking. (Lecture Notes)

            Larsen, Pettersson, Yi: UPPAAL in a Nutshell
            In Journal for Software Tools for Technology Transfer, vol 1, 1997.

            Alexandre David: UPPAAL2K: Small Tutorial

About the Speaker

Kim Guldstrand Larsen is a Professor in the Department of Computer Science at Aalborg University within the Systems and Semantics Unit. Also, he is the director of the Aalborg section of BRICS.

His research area is theoretical computer science, more precisely the semantics of nondeterminism and concurrency. His particular interest lies in validation and verification of embedded systems, real-time and hybrid systems Currently he is spending most of his research time on developing the modelchecker UPPAAL, and on the projects VVS and VHS.