Dr. Raffaella Gentilini

(AG Reaktive Systeme)

"Verification of Hybrid Automata"

Hybrid systems are characterized by the mutual interaction of continuous and discrete dynamics. For example, hybrid systems naturally arise due to the embedding of digital controllers into continuous environments, which is the case for many embedded systems.
A popular model of hybrid systems is given by hybrid automata, which consist of a finite number of states that determine a set of differential equations to restrict the values of variables with continuous values. Safety critical applications of embedded systems require to check that certain specifications hold, so that verification procedures for hybrid automata have gained high interest in the recent years. State transitions are triggered by conditions on the continuous variables. Unfortunately, a lot of problems concerning hybrid automata like checking the reachability of specified states are undecidable. For this reason, many special classes of hybrid automata have been developed for which the reachability problem can be decided.
The talk gives an overview on formal tools for modelling, automated reasoning, and verification of hybrid automata. It will also present some special classes of hybrid automata that have a decidable reachability problem. Finally, it will sketch topics of a comprehensive course of the master programme on verification of hybrid systems.

Zeit:	Montag, 09.07.2007, 17.15 Uhr
Ort:	Gebäude 48, Raum 210