JUCS - Journal of Universal Computer Science 9(2): 88-105, doi: 10.3217/jucs-009-02-0088
Moby/RT: A Tool for Specification and Verification of Real-Time Systems
expand article infoErnst-Rüdiger Olderog, Henning Dierks
‡ Department of Computing Science University of Oldenburg, Germany
Open Access
The tool Moby/RT supports the design of realtime systems at the levels of requirements, design specifications and programs. Requirements are expressed by constraint diagrams [Kleuker, 2000], design specifications by PLC-Automata [Dierks, 2000], and programs by Structured Text, a programming language dedicated for programmable logic controllers (PLCs), or by programs for LEGO Mindstorm robots. In this paper we outline the theoretical background of Moby/RT by discussing its semantic basis and its use for automatic verification by utilising the model-checker UPPAAL [Larsen et al., 1997].
real-time, specification, formal verification, requirements capture, Constraint Diagrams, PLC-Automata