Document Open Access Logo

Distributed Runtime Verification Under Partial Synchrony

Authors Ritam Ganguly, Anik Momtaz , Borzoo Bonakdarpour

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2020.20.pdf
  • Filesize: 0.63 MB
  • 17 pages

Document Identifiers

Author Details

Ritam Ganguly
  • Michigan State University, East Lansing, MI, USA
Anik Momtaz
  • Michigan State University, East Lansing, MI, USA
Borzoo Bonakdarpour
  • Michigan State University, East Lansing, MI, USA

Funding

  • Bonakdarpour, Borzoo: This work is partially sponsored by the NSF FMitF Award 1917979.

Cite As Get BibTex

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

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Distributed computing models
Keywords
  • Runtime monitoring
  • Distributed systems
  • Formal methods
  • Cassandra

Metrics

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

References

  1. A. Bauer and Y. Falcone. Decentralised LTL monitoring. Formal Methods in System Design, 48(1-2):46-93, 2016. Google Scholar
  2. A. Bauer, M. Leucker, and C. Schallhart. Runtime Verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology (TOSEM), 20(4):14:1-14:64, 2011. Google Scholar
  3. B. Bonakdarpour, P. Fraigniaud, S. Rajsbaum, D. A. Rosenblueth, and C. Travers. Decentralized asynchronous crash-resilient runtime verification. In Proceedings of the 27th International Conference on Concurrency Theory (CONCUR), pages 16:1-16:15, 2016. Google Scholar
  4. 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
  5. C. Colombo and Y. Falcone. Organising LTL monitors over distributed systems with a global clock. Formal Methods in System Design, 49(1-2):109-158, 2016. Google Scholar
  6. L. M. Danielsson and C. Sánchez. Decentralized stream runtime verification. In Proceedings of the 19th International Conference on Runtime Verification (RV), pages 185-201, 2019. Google Scholar
  7. L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 337-340, 2008. Google Scholar
  8. A. El-Hokayem and Y. Falcone. On the monitoring of decentralized specifications: Semantics, properties, analysis, and simulation. ACM Transactions on Software Engineering Methodologies, 29(1):1:1-1:57, 2020. Google Scholar
  9. V. K. Garg. Elements of distributed computing. Wiley, 2002. Google Scholar
  10. V. K. Garg. Predicate detection to solve combinatorial optimization problems. In Proceedings of the 32nd ACM Symposium on Parallelism in Algorithms and Architectures (SPAA), pages 235-245. ACM, 2020. Google Scholar
  11. V. K. Garg and C. Chase. Distributed algorithms for detecting conjunctive predicates. International Conference on Distributed Computing Systems, pages 423-430, June 1995. Google Scholar
  12. Google. Usage limits, sheets api, google developer. https://developers.google.com/sheets/api/limits. Accessed: 2020-09-09.
  13. S. Kazemloo and B. Bonakdarpour. Crash-resilient decentralized synchronous runtime verification. In Proceedings of the 37th Symposium on Reliable Distributed Systems (SRDS), pages 207-212, 2018. Google Scholar
  14. S. S. Kulkarni, M. Demirbas, D. Madappa, B. Avva, and M. Leone. Logical physical clocks. In Proceedings of the 18th International Conference on Principles of Distributed Systems, pages 17-32, 2014. Google Scholar
  15. Avinash Lakshman and Prashant Malik. Cassandra: A decentralized structured storage system. SIGOPS Oper. Syst. Rev., 44(2):35–40, April 2010. URL: https://doi.org/10.1145/1773912.1773922.
  16. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558-565, 1978. Google Scholar
  17. D. Mills. Network time protocol version 4: Protocol and algorithms specification. RFC 5905, RFC Editor, June 2010. Google Scholar
  18. N. Mittal and V. K. Garg. Techniques and applications of computation slicing. Distributed Computing, 17(3):251-277, 2005. Google Scholar
  19. M. Mostafa and B. Bonakdarpour. Decentralized runtime verification of LTL specifications in distributed systems. In Proceedings of the 29th IEEE International Parallel and Distributed Processing Symposium (IPDPS), pages 494-503, 2015. Google Scholar
  20. 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
  21. A. Pnueli. The temporal logic of programs. In Symposium on Foundations of Computer Science (FOCS), pages 46-57, 1977. Google Scholar
  22. 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
  23. Scott D. Stoller. Detecting global predicates in distributed systems with clocks. In Marios Mavronicolas and Philippas Tsigas, editors, Distributed Algorithms, pages 185-199, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  24. V. T. Valapil, S. Yingchareonthawornchai, S. S. Kulkarni, E. Torng, and M. Demirbas. Monitoring partially synchronous distributed systems using SMT solvers. In Proceedings of the 17th International Conference on Runtime Verification (RV), pages 277-293, 2017. 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