Moby/DC – A tool for model-checking parametric real-time specifications. (English) Zbl 1031.68547

Garavel, Hubert (ed.) et al., Tools and algorithms for the construction and analysis of systems. 9th international conference TACAS 2003, held as part of the joint European conferences on theory and practice of software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2619, 271-277 (2003).
Summary: 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.
For the entire collection see [Zbl 1017.00035].


68Q60 Specification and verification (program logics, model checking, etc.)


Full Text: Link