Prof. Wang Yi

MODEL CHECKING FOR REAL TIME SYSTEMS

Abstract

The theory of timed automata was invented in 1990 by Alur and Dill. In the past decade, it has been recognized as a fundamental semantic model for real time systems; various automated verification tools e.g. Kronos and UPPAAL have been developed in the framework of timed automata and applied successfully in industrial case studies. In the first part of this tutorial, I will introduce the basic theory of timed automata, including the transitional semantics, and the notion of region automata which is the key construction for decidability proof for several decision problems. In the second part of the tutorial, I will introduce UPPAAL, a tool box for automated analysis of timed automata, developed jointly by Uppsala University and Aalborg University. In particular, I will summarize the basic algorithms and data structures implemented in UPPAAL.

Contact information:
Uppsala University
Dept of Computer Systems IT
Box 325
75105,UPPSALA
Sweden

EMAIL: yi@docs.uu.se
WWW: http://www.docs.uu.se/~yi/