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.OPODIS.2020.20
URN: urn:nbn:de:0030-drops-135053
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13505/
Go to the corresponding LIPIcs Volume Portal

Ganguly, Ritam ; Momtaz, Anik ; Bonakdarpour, Borzoo

Distributed Runtime Verification Under Partial Synchrony

pdf-format:
LIPIcs-OPODIS-2020-20.pdf (0.6 MB)

Abstract

In this paper, we study the problem of runtime verification of distributed applications that do not share a global clock with respect to specifications in the linear temporal logics (LTL). Our proposed method distinguishes from the existing work in three novel ways. First, we make a practical assumption that the distributed system under scrutiny is augmented with a clock synchronization algorithm that guarantees bounded clock skew among all processes. Second, we do not make any assumption about the structure of predicates that form LTL formulas. This relaxation allows us to monitor a wide range of applications that was not possible before. Subsequently, we propose a distributed monitoring algorithm by employing SMT solving techniques. Third, given the fact that distributed applications nowadays run on massive cloud services, we extend our solution to a parallel monitoring algorithm to utilize the available computing infrastructure. We report on rigorous synthetic as well as real-world case studies and demonstrate that scalable online monitoring of distributed applications is within our reach.

BibTeX - Entry

@InProceedings{ganguly_et_al:LIPIcs:2021:13505,
  author =	{Ritam Ganguly and Anik Momtaz and Borzoo Bonakdarpour},
  title =	{{Distributed Runtime Verification Under Partial Synchrony}},
  booktitle =	{24th International Conference on Principles of Distributed Systems (OPODIS 2020)},
  pages =	{20:1--20:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-176-4},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{184},
  editor =	{Quentin Bramas and Rotem Oshman and Paolo Romano},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13505},
  URN =		{urn:nbn:de:0030-drops-135053},
  doi =		{10.4230/LIPIcs.OPODIS.2020.20},
  annote =	{Keywords: Runtime monitoring, Distributed systems, Formal methods, Cassandra}
}

Keywords: Runtime monitoring, Distributed systems, Formal methods, Cassandra
Collection: 24th International Conference on Principles of Distributed Systems (OPODIS 2020)
Issue Date: 2021
Date of publication: 25.01.2021

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