Moby/DC
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
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
Sorted by year (- Knapik, Michał; Penczek, Wojciech: Bounded model checking for parametric timed automata (2012)
- Wehrle, Martin; Kupferschmid, Sebastian: Mcta: heuristics and search for timed systems (2012)
- Hoenicke, Jochen; Maier, Patrick: Model-checking of specifications integrating processes, data and time (2005)
- Dierks, Henning; Tapken, Josef: Moby/DC -- A tool for model-checking parametric real-time specifications (2003)
- Hoenicke, Jochen; Olderog, Ernst-Rüdiger: CSP-OZ-DC: a combination of specification techniques for processes, data and time (2002)