You are cordially invited to our ACG guest lecture, given by prof. dr. Ernst-Ruediger Olderog, entitled: "Automatic Verification of Real-Time Systems with Rich Data".
We discuss how properties of reactive systems with continuous real-time constraints and complex, possibly infinite data can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data.
The systems are specified in CSP-OZ-DC, a language that 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 this language in terms of
Phase-Event-Automata. These are further translated into the input formats of the model checkers ARMC (Abstraction Refinement Model
Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory
extensions). We demonstrate this with a case study concerning emergency messages in the European Train Control System (ETCS).
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.
Prof. dr. Ernst-Ruediger Olderog is professor Correct System Design at the University of Oldenburg. He received in 1994 the Gottfried Wilhelm
Leibniz Prize which is the highest German research prize awarded by the Deutsche Forschungsgemeinschaft (DFG). He is author of various
scientific books and managing editor of the journal Acta Informatica.
We hope to see you there!
Michiel helvensteijn (SEN3)
