Search Results

Documents authored by Bonakdarpour, Borzoo

Document
DOI: 10.4230/LIPIcs.OPODIS.2020.20
Distributed Runtime Verification Under Partial Synchrony

Authors: Ritam Ganguly, Anik Momtaz, and Borzoo Bonakdarpour

Published in: LIPIcs, Volume 184, 24th International Conference on Principles of Distributed Systems (OPODIS 2020)

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.
Cite as

Ritam Ganguly, Anik Momtaz, and Borzoo Bonakdarpour. Distributed Runtime Verification Under Partial Synchrony. In 24th International Conference on Principles of Distributed Systems (OPODIS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 184, pp. 20:1-20:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ganguly_et_al:LIPIcs.OPODIS.2020.20,
  author =	{Ganguly, Ritam and Momtaz, Anik and Bonakdarpour, Borzoo},
  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 =	{Bramas, Quentin and Oshman, Rotem and Romano, Paolo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2020.20},
  URN =		{urn:nbn:de:0030-drops-135053},
  doi =		{10.4230/LIPIcs.OPODIS.2020.20},
  annote =	{Keywords: Runtime monitoring, Distributed systems, Formal methods, Cassandra}
}
Document
DOI: 10.4230/LIPIcs.OPODIS.2018.29
Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings

Authors: Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour

Published in: LIPIcs, Volume 125, 22nd International Conference on Principles of Distributed Systems (OPODIS 2018)

Abstract
Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.
Cite as

Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour. Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{mirzaie_et_al:LIPIcs.OPODIS.2018.29,
  author =	{Mirzaie, Nahal and Faghih, Fathiyeh and Jacobs, Swen and Bonakdarpour, Borzoo},
  title =	{{Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings}},
  booktitle =	{22nd International Conference on Principles of Distributed Systems (OPODIS 2018)},
  pages =	{29:1--29:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-098-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{125},
  editor =	{Cao, Jiannong and Ellen, Faith and Rodrigues, Luis and Ferreira, Bernardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2018.29},
  URN =		{urn:nbn:de:0030-drops-100896},
  doi =		{10.4230/LIPIcs.OPODIS.2018.29},
  annote =	{Keywords: Parameterized synthesis, Self-stabilization, Formal methods}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.16
Decentralized Asynchronous Crash-Resilient Runtime Verification

Authors: Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
Runtime Verification (RV) is a lightweight method for monitoring the formal specification of a system during its execution. It has recently been shown that a given state predicate can be monitored consistently by a set of crash-prone asynchronous distributed monitors, only if sufficiently many different verdicts can be emitted by each monitor. We revisit this impossibility result in the context of LTL semantics for RV. We show that employing the four-valued logic Rv-LTL will result in inconsistent distributed monitoring for some formulas. Our first main contribution is a family of logics, called Ltl2k+4, that refines Rv-Ltl incorporating 2k + 4 truth values, for each k >= 0. The truth values of Ltl2k+4 can be effectively used by each monitor to reach a consistent global set of verdicts for each given formula, provided k is sufficiently large. Our second main contribution is an algorithm for monitor construction enabling fault-tolerant distributed monitoring based on the aggregation of the individual verdicts by each monitor.
Cite as

Borzoo Bonakdarpour, Pierre Fraigniaud, Sergio Rajsbaum, David A. Rosenblueth, and Corentin Travers. Decentralized Asynchronous Crash-Resilient Runtime Verification. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 16:1-16:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{bonakdarpour_et_al:LIPIcs.CONCUR.2016.16,
  author =	{Bonakdarpour, Borzoo and Fraigniaud, Pierre and Rajsbaum, Sergio and Rosenblueth, David A. and Travers, Corentin},
  title =	{{Decentralized Asynchronous Crash-Resilient Runtime Verification}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{16:1--16:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.16},
  URN =		{urn:nbn:de:0030-drops-61856},
  doi =		{10.4230/LIPIcs.CONCUR.2016.16},
  annote =	{Keywords: Runtime monitoring, Distributed algorithms, Fault-tolerance}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact