Moby/RT: A Tool for Specification and Verification of Real-Time Systems
Ernst-Rüdiger Olderog (Department of Computing Science University of Oldenburg, Germany)
Henning Dierks (Department of Computing Science University of Oldenburg, Germany)
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: Constraint Diagrams, PLC-Automata, formal verification, real-time, requirements capture, specification
Categories: D.2.1, D.2.2, D.2.4, D.4.7, F.3.1, F.4.1