[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

First-order temporal logic monitoring with BDDs

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

A Preface to the special issue FMCAD 2017 to this article was published on 18 January 2021

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6

Similar content being viewed by others

Notes

  1. DejaVu is available at https://github.com/havelund/dejavu.

  2. \(\upgamma \, [ x \mapsto a ]\) is the overriding of \(\upgamma \) with the binding \([ x \mapsto a ]\).

  3. This restriction from the theory and algorithm presented above is made because our experience shows that this is by far the most common case.

  4. Traces accepted by the tool are concretely in CSV format. For example the first event is a single line of the form: open,input,read.

References

  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–364

  2. Alpern B, Schneider FB (1987) Recognizing safety and liveness. Distrib Comput 2(3):117–126

    Article  Google Scholar 

  3. Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification, VMCAI, LNCS Volume 2937. Springer

  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. Springer

  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. Springer

  6. Basin DA, Klaedtke F, Müller S, Zalinescu E (2015) Monitoring metric first-order temporal properties. J ACM 62(2):45

    Article  MathSciNet  Google Scholar 

  7. Bensalem S, Havelund K (2006) Dynamic deadlock analysis of multi-threaded programs. In: Haifa verification conference, Haifa, Israel, LNCS volume 3875. Springer

  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–213

    Article  MathSciNet  Google Scholar 

  9. Bryant RE (1992) Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Comput Surv 24(3):293–318

    Article  Google Scholar 

  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. 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–174

  12. Decker N, Leucker M, Thoma D (2016) Monitoring modulo theories. J Softw Tools Technol Transf 18(2):205–225

    Article  Google Scholar 

  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. Springer

  14. Hallé S, Villemaire R (2012) Runtime enforcement of web service message contracts with data. IEEE Trans Serv Comput 5(2):192–206

    Article  Google Scholar 

  15. Havelund K (2015) Rule-based runtime verification revisited. J Softw Tools Technol Transf 17(2):143–170

    Article  Google Scholar 

  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, Vienna

  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. Springer

  18. Havelund K, Rosu G (2002) Synthesizing monitors for safety properties. In: TACAS, pp 342–356

  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–110

  20. JavaBDD. http://javabdd.sourceforge.net

  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). Elsevier

  22. Kupferman O, Vardi MY (2001) Model checking of safety properties. Form Methods Syst Des 19(3):291–314

    Article  Google Scholar 

  23. Manna Z, Pnueli A (1991) Completing the temporal picture. Theor Comput Sci 83:91–130

    Article  Google Scholar 

  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–289

    Article  Google Scholar 

  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). Springer

  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–411

    Article  Google Scholar 

  27. Whaley J, Avots D, Carbin M, Lam MS (2005) Using Datalog with binary decision diagrams for program analysis. In: APLAS, pp 97–118

Download references

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.

Author information

Authors and Affiliations

  1. Jet Propulsion Laboratory, California Institute of Technology, Pasadena, CA, USA

    Klaus Havelund

  2. Department of Computer Science, Bar Ilan University, Ramat Gan, Israel

    Doron Peled

  3. Boston University, Boston, MA, USA

    Dogan Ulus

Authors
  1. Klaus Havelund
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Doron Peled
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dogan Ulus
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Klaus Havelund, Doron Peled or Dogan Ulus.

Additional information

The research performed by the first author was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration. The research performed by the second author was partially funded by Israeli Science Foundation Grant 2239/15: “Runtime Measuring and Checking of Cyber Physical Systems”.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Havelund, K., Peled, D. & Ulus, D. First-order temporal logic monitoring with BDDs. Form Methods Syst Des 56, 1–21 (2020). https://doi.org/10.1007/s10703-018-00327-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-018-00327-4

Keywords

Search

Navigation