Lecture by prof. dr. Ernst-Ruediger Olderog (University Oldenburg)

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".
  • When 27-09-2011 from 11:30 to 12:30 (Europe/Amsterdam / UTC200)
  • Where L120 (lecture room first floor, new wing)
  • Web Visit external website
  • Add event to calendar iCal

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)