Moby/RT: A Tool for Specification and Verification of Real-Time Systems
Дата
Авторы
Olderog,Ernst-Rüdiger
Dierks,Henning
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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