License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2015.590
URN: urn:nbn:de:0030-drops-56194
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5619/
Go to the corresponding LIPIcs Volume Portal

Basin, David ; Klaedtke, Felix ; Zalinescu, Eugen

Failure-aware Runtime Verification of Distributed Systems

pdf-format:
3.pdf (0.5 MB)

Abstract

Prior runtime-verification approaches for distributed systems are limited as they do not account for network failures and they assume that system messages are received in the order they are sent. To overcome these limitations, we present an online algorithm for verifying observed system behavior at runtime with respect to specifications written in the real-time logic MTL that efficiently handles out-of-order message deliveries and operates in the presence of failures. Our algorithm uses a three-valued semantics for MTL, where the third truth value models knowledge gaps, and it resolves knowledge gaps as it propagates Boolean values through the formula structure. We establish the algorithm's soundness and provide completeness guarantees. We also show that it supports distributed system monitoring, where multiple monitors cooperate and exchange their observations and conclusions.

BibTeX - Entry

@InProceedings{basin_et_al:LIPIcs:2015:5619,
  author =	{David Basin and Felix Klaedtke and Eugen Zalinescu},
  title =	{{Failure-aware Runtime Verification of Distributed Systems}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{590--603},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Prahladh Harsha and G. Ramalingam},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5619},
  URN =		{urn:nbn:de:0030-drops-56194},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.590},
  annote =	{Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication}
}

Keywords: Runtime verification, monitoring algorithm, real-time logics, multi-valued semantics, distributed systems, asynchronous communication
Collection: 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)
Issue Date: 2015
Date of publication: 14.12.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI