Institute of Computer Languages
Compilers and Languages Group
on
| Date: | Thursday, December 13th, 2007 |
|---|---|
| Time: | 14:00 (c.t.) |
| Location: | TU Wien, Elektrotechnik, EI 5 Hochenegg-Hörsaal, Gußhausstraße 25-29 (Altbau), 2. Stock |
We discuss how properties of high-level specifications of real-time systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data. As specification language we consider CS-OZ-DC, which integrates concepts from Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC). Our approach to automatic verification rests on a compositional semantics of these languages in terms of Phase-Event-Automata. These are translated into Transition Constraint Systems which serve as an input language of an abstraction refinement model checker which can handle constraints covering both real-time and infinite data. We demonstrate this with a case study concerning emergency messages in the European Train Control System (ETCS). For CSP-OZ-DC we also discuss a UML profile and tool support.
The talk is based on the project "Beyond Timed Automata" carried out in the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbrücken, funded by the German Research Council (DFG): see also www.avacs.org.
Ernst-Rüdiger Olderog obtained his diploma, doctoral degree, and habilitation in Computer Science from the University of Kiel in the years 1979, 1981 and 1989. During 1981-1983 he was a visiting scientist in the Programming Research Group at Oxford University. He has been visiting professor at the Universities of Saarbrücken and Amsterdam, and at ETH Zürich. Since 1989 he is a professor of Computing Science at the University of Oldenburg. His research interest is in the area of specification, design, and verification of programs, reactive and real-time systems. In 1994 he was awarded the Leibniz Prize of the DFG. During 1995-2005 he was chairman of the IFIP Working Group 2.2 on Formalization of Programming Concepts. Since 2000 he is Editor-in-Chief of the journal Acta Informatica. (http://csd.informatik.uni-oldenburg.de/)