Document Open Access Logo

Failure-aware Runtime Verification of Distributed Systems

Authors David Basin, Felix Klaedtke, Eugen Zalinescu

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2015.590.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

David Basin
Felix Klaedtke
Eugen Zalinescu

Cite AsGet BibTex

David Basin, Felix Klaedtke, and Eugen Zalinescu. Failure-aware Runtime Verification of Distributed Systems. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 590-603, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.FSTTCS.2015.590

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.
Keywords
  • Runtime verification
  • monitoring algorithm
  • real-time logics
  • multi-valued semantics
  • distributed systems
  • asynchronous communication

Metrics

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

References

  1. R. Alur and T. A. Henzinger. Logics and models of real time: A survey. In Proceedings of the 1991 REX Workshop on Real Time: Theory in Practice, volume 600 of Lect. Notes Comput. Sci. , pages 74-106. Springer, 1992. Google Scholar
  2. D. Basin, F. Klaedtke, and E. Zălinescu. Algorithms for monitoring real-time properties. In Proceedings of the 2nd International Conference on Runtime Verification (RV), volume 7186 of Lect. Notes Comput. Sci. , pages 260-275. Springer, 2011. Google Scholar
  3. A. Bauer and Y. Falcone. Decentralised LTL monitoring. In Proceedings of the 18th International Symposium on Formal Methods (FM), volume 7436 of Lect. Notes Comput. Sci. , pages 85-100. Springer, 2012. Google Scholar
  4. A. Bauer, M. Leucker, and C. Schallhart. Comparing LTL semantics for runtime verification. J. Logic Comput. , 20(3):651-674, 2010. Google Scholar
  5. A. Bauer, M. Leucker, and C. Schallhart. Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Meth. , 20(4):14, 2011. Google Scholar
  6. M. Chechik, B. Devereux, S. Easterbrook, and A. Gurfinkel. Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Meth. , 12(4), 2003. Google Scholar
  7. F. Cristian and C. Fetzer. The timed asynchronous distributed system model. IEEE Trans. Parallel Distrib. Syst., 10(6):642-657, 1999. Google Scholar
  8. Y. Falcone, T. Cornebize, and J.-C. Fernandez. Efficient and generalized decentralized monitoring of regular languages. In Proceedings of the 34th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), volume 8461 of Lect. Notes Comput. Sci. , pages 66-83. Springer, 2014. Google Scholar
  9. M. J. Fischer, N. A. Lynch, and M. S. Paterson. Impossibility of distributed consensus with one faulty process. J. ACM, 32(2):374-382, 1985. Google Scholar
  10. S. C. Kleene. Introduction to Metamathematics. D. Van Nostrand, Princeton, 1950. Google Scholar
  11. R. Koymans. Specifying real-time properties with metric temporal logic. Real-Time Syst. , 2(4):255-299, 1990. Google Scholar
  12. L. Lamport. Time, clocks, and the ordering of events in a distributed system. Commun. ACM, 21(7):558-565, 1978. Google Scholar
  13. O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems (FORMATS) and on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), volume 3253 of Lect. Notes Comput. Sci. , pages 152-166. Springer, 2004. Google Scholar
  14. D. L. Mills. Improved algorithms for synchronizing computer network clocks. IEEE/ACM Trans. Netw., 3(3):245-254, 1995. Google Scholar
  15. M. Mostafa and B. Bonakdarbour. 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. IEEE Computer Society, 2015. Google Scholar
  16. Network time protocol. www.ntp.org, webpage accessed on March 26, 2015. Google Scholar
  17. A. Pnueli and A. Zaks. PSL model checking and run-time verification via testers. In Proceedings of the 14th International Symposium on Formal Methods (FM), volume 4085 of Lect. Notes Comput. Sci. , pages 573-586. Springer, 2008. Google Scholar
  18. T. Scheffel and M. Schmitz. Three-valued asynchronous distributed runtime verification. In Proceedings of the 12th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMCODE), pages 52-61. IEEE Computer Society, 2014. 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. IEEE Computer Society, 2004. Google Scholar
  20. P. Thati and G. Roşu. Monitoring algorithms for metric temporal logic specifications. In Proceedings of the 4th Workshop on Runtime Verification (RV), volume 113 of Elec. Notes Theo. Comput. Sci. , pages 145-162. Elsevier Science Inc. , 2005. 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 Imprint Privacy Contact