MOBY/DC― A Tool for Model-Checking Parametric Real-Time Specifications

摘要

We define an operational subset of Duration Calculus, called phase automata, which serves as an intermediate language for the analysis and verification of real-time system descriptions that contain timing parameters. We introduce the tool MoBY/DC which implements a model-checking algorithm for phase automata. The algorithm applies compositional model-checking techniques and handles parameters by built-in procedures or by a link to CLP(R). Due to the parameters the model-checking problem is undecidable in general. Hence, we have to accept that the results are overapproximations only in order to guarantee termination. The overapproximation together with the compositional technique makes the model-checker especially well suited for proving the absence of error traces instead of finding them.