Sciweavers

FAC
2008

Model checking Duration Calculus: a practical approach

13 years 3 months ago
Model checking Duration Calculus: a practical approach
Abstract. Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).
Roland Meyer, Johannes Faber, Jochen Hoenicke, And
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where FAC
Authors Roland Meyer, Johannes Faber, Jochen Hoenicke, Andrey Rybalchenko
Comments (0)