Three-Valued Asynchronous Distributed Runtime Verification

Torben Scheffel, Malte Schmitz


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.

Original languageEnglish
Title of host publication 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)
Number of pages10
Publication date01.10.2014
ISBN (Print)978-147995338-7
Publication statusPublished - 01.10.2014
Event12th ACM/IEEE International Conference on Methods and Models for System Design
- Lausanne, Switzerland
Duration: 19.10.201421.10.2014
Conference number: 109325


Dive into the research topics of 'Three-Valued Asynchronous Distributed Runtime Verification'. Together they form a unique fingerprint.

Cite this