Advertisement

First-order temporal logic monitoring with BDDs

  • Klaus HavelundEmail author
  • Doron PeledEmail author
  • Dogan UlusEmail author
Article
  • 36 Downloads

Abstract

Runtime verification is aimed at analyzing execution traces stemming from a running program or system. The traditional purpose is to detect the lack of conformance with respect to a formal specification. Numerous efforts in the field have focused on monitoring parametric specifications, where events carry data, and formulas can refer to such. Since a monitor for such specifications has to store observed data, the challenge is to have an efficient representation and manipulation of Boolean operators, quantification, and lookup of data. The fundamental problem is that the actual values of the data are not necessarily bounded or provided in advance. In this work we explore the use of binary decision diagrams for representing observed data. Our experiments show a substantial improvement in performance compared to related work.

Keywords

Past time temporal logic Data BDDs 

Notes

Acknowledgements

We would like to thank Oded Maler for a discussion on representing sets using BDDs. We also thank Eugen Zălinescu for discussions concerning monitorability of MonPoly formulas. Finally, we thank the reviewers of this article for their useful comments.

References

  1. 1.
    Allan C, Avgustinov P, Christensen AS, Hendren LJ, Kuzins S, Lhotak O, de Moor O, Sereni D, Sittampalam G, Tibble J (2005) Adding trace matching with free variables to AspectJ. In: OOPSLA, pp 345–364Google Scholar
  2. 2.
    Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117–126CrossRefzbMATHGoogle Scholar
  3. 3.
    Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification, VMCAI, LNCS Volume 2937. SpringerGoogle Scholar
  4. 4.
    Barringer H, Havelund K (2011) TraceContract: a scala DSL for trace analysis. In: Proceedings of the 17th international symposium on formal methods (FM’11), LNCS volume 6664. SpringerGoogle Scholar
  5. 5.
    Barringer H, Rydeheard D, Havelund K (2007) Rule systems for run-time monitoring: from Eagle to RuleR. In: Proceedings of the 7th international workshop on runtime verification (RV’07), LNCS volume 4839. SpringerGoogle Scholar
  6. 6.
    Basin DA, Klaedtke F, Müller S, Zalinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):45MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Bensalem S, Havelund K (2006) Dynamic deadlock analysis of multi-threaded programs. In: Haifa verification conference, Haifa, Israel, LNCS volume 3875. SpringerGoogle Scholar
  8. 8.
    Bryant RE (1991) On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication. IEEE Trans Comput 40(2):205–213MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318CrossRefGoogle Scholar
  10. 10.
    Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1990) Symbolic model checking: \(10^{20}\) states and beyond. In: Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp. 428–439.  https://doi.org/10.1109/LICS.1990.113767
  11. 11.
    D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z (2005) LOLA: runtime monitoring of synchronous systems. In: TIME, pp 166–174Google Scholar
  12. 12.
    Decker N, Leucker M, Thoma D (2016) Monitoring modulo theories. J Softw Tools Technol Transf 18(2):205–225CrossRefGoogle Scholar
  13. 13.
    Goubault-Larrecq J, Olivain J (2008) A Smell of ORCHIDS. In: Proceedings of the 8th international workshop on runtime verification (RV’08), LNCS volume 5289. SpringerGoogle Scholar
  14. 14.
    Hallé S, Villemaire R (2012) Runtime enforcement of web service message contracts with data. IEEE Trans Serv Comput 5(2):192–206CrossRefGoogle Scholar
  15. 15.
    Havelund K (2015) Rule-based runtime verification revisited. J Softw Tools Technol Transf 17(2):143–170CrossRefGoogle Scholar
  16. 16.
    Havelund K, Peled D, Ulus D (2017) First-order temporal logic monitoring with BDDs. In: 17th conference on formal methods in computer-aided design (FMCAD 2017), 2–6 Oct, 2017. IEEE, ViennaGoogle Scholar
  17. 17.
    Havelund K, Reger G, Thoma D, Zălinescu E (2018) Monitoring events that carry data. In: Bartocci E, Falcone Y (eds) Lectures on runtime verification-introductory and advanced topics, LNCS volume 10457. SpringerGoogle Scholar
  18. 18.
    Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: TACAS, pp 342–356Google Scholar
  19. 19.
    Henriksen JG, Jensen JL, Jorgensen ME, Klarlund N, Paige R, Rauhe T, Sandholm A (1995) Mona: monadic second-order logic in practice. In: TACAS, pp 89–110Google Scholar
  20. 20.
  21. 21.
    Kim M, Kannan S, Lee I, Sokolsky O (2001) Java-MaC: a run-time assurance tool for Java. In: Proceedings of the 1st international workshop on runtime verification (RV’01), ENTCS, 55(2). ElsevierGoogle Scholar
  22. 22.
    Kupferman O, Vardi MY (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291–314CrossRefzbMATHGoogle Scholar
  23. 23.
    Manna Z, Pnueli A (1991) Completing the temporal picture. Theor Comput Sci 83:91–130CrossRefzbMATHGoogle Scholar
  24. 24.
    Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2011) An overview of the MOP runtime verification framework. J Softw Tools Technol Transf 14:249–289CrossRefGoogle Scholar
  25. 25.
    Reger G, Cruz H, Rydeheard D (2015) MarQ: monitoring at runtime with QEA. In: Proceedings of the 21st international conference on tools and algorithms for the construction and analysis of systems (TACAS 2015). SpringerGoogle Scholar
  26. 26.
    Savage S, Burrows M, Nelson G, Sobalvarro P, Anderson T (1997) Eraser: a dynamic data race detector for multithreaded programs. ACM Trans Comput Syst 15(4):391–411CrossRefGoogle Scholar
  27. 27.
    Whaley J, Avots D, Carbin M, Lam MS (2005) Using Datalog with binary decision diagrams for program analysis. In: APLAS, pp 97–118Google Scholar

Copyright information

© Springer Science+Business Media, LLC, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Jet Propulsion Laboratory, California Institute of TechnologyPasadenaUSA
  2. 2.Department of Computer ScienceBar Ilan UniversityRamat GanIsrael
  3. 3.Boston UniversityBostonUSA

Personalised recommendations