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.