Three-Valued Asynchronous Distributed Runtime Verification
Conference Paper published in October 2014 at the International Conference on Formal Methods and Models for System Design (MEMOCODE). I wrote this paper together with my colleague Torben Scheffel at the Institute for Software Engineering and Programming Languages (ISP) at the the Universität zu Lübeck.
Abstract This paper studies runtime verification of distributed asynchronous systems and presents a monitor generation procedure for this purpose, which allows three-valued monitoring. The properties used in the monitors are specified in a logic that was newly created for this purpose and is called Distributed Temporal Logic (DTL). DTL combines the three-valued Linear Temporal Logic (LTL3) with the past-time Distributed Temporal Logic (ptDTL), which allows to mark subformulas for remote evaluation. The monitor generation presented in this paper is based on an adopted version of the LTL3 monitor generation, which integrates the ptDTL monitor construction. The aim of this new procedure is to increase the amount of monitorable properties compared to the properties monitorable with ptDTL. Runtime verification using this new monitoring has been implemented on LEGO Mindstorms NXT robots communicating via Bluetooth.
Weitere Informationen und die im Rahmen der Arbeit entwickelte Software zum Download finden sich auf der Website des Projektes LEGO® meets RV.
Downloads
3D-Modell des LEGO®-Aufbaus
Die verwendeten LEGO®-Mindstorms-Bausätze wurden nach der Beendigung der Arbeit an LEGO® meets RV für andere Projekte benötigt. Um den LEGO®-Aufbau trotzdem zu archivieren, habe ich ein 3D-Modell mit dem LEGO® Digital Designer angefertigt. In dem Modell sind auch zwei zusätzliche Roboterarme enthalten, die im Video und im Screenshot oben nicht zu sehen sind. Die waren eigentlich dazu gedacht, verschiedene Werkstücke, die über das Förderband laufen, zu sortieren. Aber dazu ist es irgendwie nie gekommen. Das Modell ist primär zu dokumentarischen Zwecken und nicht unbedingt für den Nachbau gedacht. Beim Erzeugen des Modells ist mir mal wieder aufgefallen, dass man viele Details noch deutlich weiter verbessern müsste…
Downloads
Verteilte Laufzeitverifikation auf eingebetteten Systemen
Masterarbeit am Institut für Softwaretechnik und Programmiersprachen (ISP) der Universität zu Lübeck. Ausgegeben und betreut von Prof. Dr. Martin Leucker.
Kurzfassung In dieser Arbeit werden Varianten der linearen Temporallogik (LTL) für den Einsatz zur Laufzeitverifikation verteilter, asynchroner, eingebetteter Systeme und die zugehörigen Monitorkonstruktionen untersucht und implementiert. Dazu wird eine verteilte Temporallogik mit Vergangenheitsoperatoren (ptDTL) und eine auf dreiwertiger Temporallogik (LTL3) basierende, verteilte Temporallogik (fDTL) sowie eine synchronisierte Variante dieser Logik (fSDTL) verwendet. Für die dreiwertigen Logiken werden neue Automatenmodelle entwickelt und mit bekannten Monitorkonstruktionen verglichen. Als eingebettete Systeme kommen dabei Roboter von LEGO Mindstorms zum Einsatz, die in dem C-Dialekt NXC programmiert werden. Im Rahmen dieser Arbeit wurde ein Scala-Programm zur Monitorinjektion über Programmtransformation entwickelt. Das Programm liest den C-Quelltext mehrerer Roboter ein, parst die in Kommentaren enthaltenen Annotationen und ergänzt die für die verteilte Laufzeitverifikation notwendigen Routinen im Quelltext. Anhand dieser Software werden die verschiedenen Monitorkonstruktionen und Techniken der Zustandsgenerierung im praktischen Einsatz verglichen.
Abstract This thesis analyses and implements modifications of Linear Temporal Logic (LTL) and monitor generation procedures for these logics that can be used for runtime verification of distributed asynchronous embedded systems. For this purpose a distributed temporal logic with past operators (ptDTL) and a distributed temporal logic (fDTL) which is based on the three-valued temporal logic (LTL3) are used. Furthermore a synchronized modification of this logic (fSDTL) is studied. Especially for the three-valued logics new monitor generation procedures using automata models are developed and compared with already known procedures. LEGO Mindstorms robots programmed using the C dialect NXC are used as embedded systems. Within the scope of this thesis a Scala application was developed which performs monitor injection via program transformation. It takes the C source code of multiple robots, parses the annotations contained in comments and adds the routines needed for distributed runtime verification to the source code. Using this software, the different monitor generation procedures and ways of state generation are compared in practice.
