Three-Valued Asynchronous Distributed Runtime Verification

Torben Scheffel; Malte Schmitz

doi:10.1109/MEMCOD.2014.6961843

Three-Valued Asynchronous Distributed Runtime Verification

Torben Scheffel, Malte Schmitz

Institute of Software Engineering and Programming Languages

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 (LTL₃) 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 LTL₃ 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 language	English
Title of host publication	2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)
Number of pages	10
Publisher	IEEE
Publication date	01.10.2014
Pages	52-61
ISBN (Print)	978-147995338-7
DOIs	https://doi.org/10.1109/MEMCOD.2014.6961843
Publication status	Published - 01.10.2014
Event	12th ACM/IEEE International Conference on Methods and Models for System Design - Lausanne, Switzerland Duration: 19.10.2014 → 21.10.2014 Conference number: 109325

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1109/MEMCOD.2014.6961843

Cite this

@inproceedings{3dc91b70c0d14399bff1ed26d59ee7c4,

title = "Three-Valued Asynchronous Distributed Runtime Verification",

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.",

author = "Torben Scheffel and Malte Schmitz",

year = "2014",

month = oct,

day = "1",

doi = "10.1109/MEMCOD.2014.6961843",

language = "English",

isbn = "978-147995338-7",

series = "IEEE Proceedings",

publisher = "IEEE",

pages = "52--61",

booktitle = "2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)",

note = "12th ACM/IEEE International Conference on Methods and Models for System Design <br/>, MEMOCODE 2014 ; Conference date: 19-10-2014 Through 21-10-2014",

}

Scheffel, T & Schmitz, M 2014, Three-Valued Asynchronous Distributed Runtime Verification. in 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE). IEEE Proceedings, IEEE, pp. 52-61, 12th ACM/IEEE International Conference on Methods and Models for System Design
, Lausanne, Switzerland, 19.10.14. https://doi.org/10.1109/MEMCOD.2014.6961843

TY - GEN

T1 - Three-Valued Asynchronous Distributed Runtime Verification

AU - Scheffel, Torben

AU - Schmitz, Malte

N1 - Conference code: 109325

PY - 2014/10/1

Y1 - 2014/10/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-84916598486&origin=inward&txGid=0a6cfcec62bac089563c70cefcc98d23

U2 - 10.1109/MEMCOD.2014.6961843

DO - 10.1109/MEMCOD.2014.6961843

M3 - Conference contribution

SN - 978-147995338-7

T3 - IEEE Proceedings

SP - 52

EP - 61

BT - 2014 Twelfth ACM/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)

PB - IEEE

T2 - 12th ACM/IEEE International Conference on Methods and Models for System Design <br/>

Y2 - 19 October 2014 through 21 October 2014

ER -

Three-Valued Asynchronous Distributed Runtime Verification

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this