Model Checking Duration Calculus: A Practical Approach
Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. The authors propose a translation algorithm that advances the applicability of model checking tools to real world applications. Their algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. They implemented the algorithm as part of their tool chain for the automated verification of systems comprising data, communication, and real-time aspects.