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