Document Open Access Logo

Decentralized Asynchronous Crash-Resilient Runtime Verification

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.16.pdf
  • Filesize: 0.65 MB
  • 15 pages

Document Identifiers

Author Details

Borzoo Bonakdarpour
Pierre Fraigniaud
Sergio Rajsbaum
David A. Rosenblueth
Corentin Travers

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CONCUR.2016.16

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.

Subject Classification

Keywords
  • Runtime monitoring
  • Distributed algorithms
  • Fault-tolerance

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Yehuda Afek, Hagit Attiya, Danny Dolev, Eli Gafni, Michael Merritt, and Nir Shavit. Atomic snapshots of shared memory. Journal of the ACM, 40(4):873-890, 1993. Google Scholar
  2. Hagit Attiya and Jennifer Welch. Distributed Computing: Fundamentals, Simulations, and Advanced Topics. Wiley, 2004. Google Scholar
  3. A. Bauer, M. Leucker, and C. Schallhart. Comparing LTL Semantics for Runtime Verification. Journal of Logic and Computation, 20(3):651-674, 2010. Google Scholar
  4. A. Bauer, M. Leucker, and C. Schallhart. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM), 20(4):14, 2011. Google Scholar
  5. A. K. Bauer and Y. Falcone. Decentralised LTL monitoring. In Proceedings of the 18th International Symposium on Formal Methods (FM), pages 85-100, 2012. Google Scholar
  6. S. Berkovich, B. Bonakdarpour, and S. Fischmeister. GPU-based runtime verification. In Proceedings of the 27th IEEE International Parallel and Distributed Processing Symposium (IPDPS), pages 1025-1036, 2013. Google Scholar
  7. H. Chauhan, V. K. Garg, A. Natarajan, and N. Mittal. A distributed abstraction algorithm for online predicate detection. In Proceedings of the 32nd IEEE Symposium on Reliable Distributed Systems (SRDS), pages 101-110, 2013. Google Scholar
  8. C. Colombo and Y. Falcone. Organising LTL monitors over distributed systems with a global clock. In Proceedings of the 14th International Conference on Runtime Verification (RV), pages 140-155, 2014. Google Scholar
  9. M. J. Fischer, N. .A. Lynch, and M. S. Peterson. Impossibility of distributed consensus with one faulty processor. Journal of the ACM, 32(2):373-382, 1985. Google Scholar
  10. P. Fraigniaud, S. Rajsbaum, and C. Travers. On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In Proceedings of the 5th International Conference on Runtime Verification (RV), pages 92-107, 2014. Google Scholar
  11. Pierre Fraigniaud, Sergio Rajsbaum, Matthieu Roy, and Corentin Travers. The opinion number of set-agreement. In Proceedings of the 18th International Conference on Principles of Distributed Systems (OPODIS), pages 155-170, 2014. Google Scholar
  12. Pierre Fraigniaud, Sergio Rajsbaum, and Corentin Travers. Locality and checkability in wait-free computing. Distributed Computing, 26(4):223-242, 2013. URL: http://dx.doi.org/10.1007/s00446-013-0188-x,
  13. M.H. Herlihy, D. Kozlov, and S. Rajsbaum. Distributed Computing Through Combinatorial Topology. Morgan Kaufmann-Elsevier, 2013. Google Scholar
  14. Z. Manna and A. Pnueli. Temporal verification of reactive systems - safety. Springer, 1995. Google Scholar
  15. N. Mittal and V. K. Garg. Techniques and applications of computation slicing. Distributed Computing, 17(3):251-277, 2005. Google Scholar
  16. M. Mostafa and B. Bonakdarpour. Decentralized runtime verification of LTL specifications in distributed systems. In Proceedings of the 29th International Parallel and Distributed Processing Symposium (IPDPS), pages 494-503, 2015. Google Scholar
  17. V. A. Ogale and V. K. Garg. Detecting temporal logic predicates on distributed computations. In Proceedings of the 21st International Symposium on Distributed Computing (DISC), pages 420-434, 2007. Google Scholar
  18. A. Pnueli and A. Zaks. PSL Model Checking and Run-Time Verification via Testers. In 14th Int. Symp. on Formal Methods (FM), pages 573-586, 2006. Google Scholar
  19. K. Sen, A. Vardhan, G. Agha, and G.Rosu. Efficient decentralized monitoring of safety in distributed systems. In Proceedings of the 26th International Conference on Software Engineering (ICSE), pages 418-427, 2004. Google Scholar
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