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

Corresponding author: Ernst-Rüdiger Olderog ( olderog@informatik.uni-oldenburg.de )

© Ernst-Rüdiger Olderog, Henning Dierks.
This article is freely available under the J.UCS Open Content License.
Citation: Olderog E-R, Dierks H (2003) Moby/RT: A Tool for Specification and Verification of Real-Time Systems. JUCS - Journal of Universal Computer Science 9(2): 88-105. https://doi.org/10.3217/jucs-009-02-0088
Open Access
Abstract
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].
Keywords
real-time, specification, formal verification, requirements capture, Constraint Diagrams, PLC-Automata