[Date Prev][Date Next][Date Index]

Talk Announcement: Games, Time, and Probabilities: Models and Algorithms for System Design and Analysis - Thomas Henzinger

Date: Friday, May 6th 2005, 17:00 - 18:30
Place: lecture room EI 8, Gußhausstraße 27-29, ground floor, new building


Das Wolfgang Pauli Institut und das Institut für Informationssysteme der TU Wien laden gemeinsam mit der Österreichischen Computergesellschaft (OCG) zu u.a. Vortrag ein. Anschließend findet die Vorstellung der Aktivitäten des Institutes für Informationssysteme der TU Wien im Rahmen des WPI statt.

Games, Time, and Probabilities: Models and Algorithms for System Design and Analysis

Tom Henzinger
EPFL and UC Berkeley

Zeit:  6.Mai 2005, 17:00 ? 18:30
Ort:   EI 8, Gußhausstraße 27-29, Erdgeschoß Neubau

Abstract: Digital technology, from medical implants to drive-by-wire systems, is increasingly deployed in safety-critical situations. This calls for systematic design and verification methodologies that can cope with three major sources of system complexity: concurrency, heterogeneity, and uncertainty. We advocate a two-step process: formal modeling followed by algorithmic analysis (or, "model building" followed by "model checking"). We model the components of a concurrent system as potential collaborators or adversaries in a multiplayer game with a given objective, such as system safety. The real-time and reactive aspects of embedded software are modeled by hybrid dynamical systems that combine both discrete state transitions and continuous state evolutions. Uncertainty in the environment is naturally modeled by stochastic processes. While the model checking of boolean systems is now standard practice in hardware verification, recently much progress has been made also in model checking software and embedded systems. These algorithms must cope with the infinite aspects of the models outlined above, including an unbounded number of concurrent processes, nonboolean data, and real numbers for representing time and probabilities. We present a general framework for constructing such model checkers which is based on three paradigms: the use of fixed-point computations on symbolic constraints for exploring nonboolean state spaces, the use of lazy abstraction refinement for automatically adjusting the precision of the algorithm, and the use of assume-guarantee reasoning for automatically dividing verification tasks into proof obligations about individual system components. We have built several model checkers that implement these paradigms for various applications, most recently Blast (the Berkeley Lazy Abstraction Software checking Tool), which automatically detects races in multithreaded C programs.

Short Biography: Tom Henzinger is Professor of Computer and Communication Sciences at the EPFL in Lausanne, Switzerland, and Professor of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He holds a Dipl.-Ing. degree in Computer Science from the Johannes Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, and a Ph.D. degree in Computer Science from Stanford University (1991). He was an Assistant Professor of Computer Science at Cornell University (1992-95), and a Director of the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999). His research focuses on modern systems theory, especially formalisms and tools for the component-based and hierarchical design, implementation, and verification of embedded, real-time, and hybrid systems. His HyTech tool was the first model checker for mixed discrete-continuous systems.