Skip to main content
SpringerLink
Log in

Accelerated Runtime Verification of LTL Specifications with Counting Semantics

  • Conference paper
  • First Online:
Runtime Verification (RV 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10012))

Included in the following conference series:

Abstract

This paper presents a novel and efficient parallel algorithm for runtime verification of an extension of Ltl that allows for nested quantifiers subject to numerical constraints. Such constraints are useful in evaluating thresholds (e.g., expected uptime of a web server). Our algorithm uses the MapReduce programming model to split a program trace into variable-based clusters at run time. Each cluster is then mapped to its respective monitor instances, verified, and reduced collectively on a multi-core CPU or the GPU. Our experiments on real-world case studies show that the algorithm imposes negligible monitoring overhead.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Barre, B., Klein, M., Soucy-Boivin, M., Ollivier, P.-A., Hallé, S.: MapReduce for Parallel trace validation of LTL properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 184–198. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_20

    Chapter  Google Scholar 

  2. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Program monitoring with LTL in eagle. In: 2004 Proceedings of the 18th International Parallel and Distributed Processing Symposium, p. 264. IEEE (2004)

    Google Scholar 

  3. Basin, D., Caronni, G., Ereth, S., Harvan, M., Klaedtke, F., Mantel, H.: Scalable offline monitoring. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 31–47. Springer, Heidelberg (2014). doi:10.1007/978-3-319-11164-3_4

    Google Scholar 

  4. Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Formal Methods Syst. Des. 46(3), 262–285 (2015)

    Article  MATH  Google Scholar 

  5. Bauer, A., Küster, J.-C., Vegliach, G.: From propositional to first-order monitoring. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 59–75. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  6. Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Logic Comput. 20(3), 651–674 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  7. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: GPU-based runtime verification. In: IEEE International Parallel and Distributed Processing Symposium (IPDPS), pp. 1025–1036 (2013)

    Google Scholar 

  8. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Formal Methods Syst. Des. 46(3), 317–348 (2015)

    Article  MATH  Google Scholar 

  9. Chen, F., Roşu, G.: Parametric trace slicing and monitoring. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 246–261. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  10. d’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), pp. 166–174. IEEE (2005)

    Google Scholar 

  11. Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  12. Drago, I., Mellia, M., Munafo, M.M., Sperotto, A., Sadre, R., Pras, A.: Inside dropbox: understanding personal cloud storage services. In: Proceedings of the 2012 ACM Conference on Internet Measurement Conference, pp. 481–494. ACM (2012)

    Google Scholar 

  13. Jin, D., Meredith, P.O., Lee, C., Rosu, G.: JavaMOP: efficient parametric runtime monitoring framework. In: 2012 34th International Conference on Software Engineering (ICSE), pp. 1427–1430, June 2012

    Google Scholar 

  14. Laroussinie, F., Meyer, A., Petonnet, E.: Counting LTL. In; Proceedings of the 2010 17th International Symposium on Temporal Representation and Reasoning, TIME 2010, pp. 51–58. IEEE Computer Society, Washington, DC (2010)

    Google Scholar 

  15. Libkin, L.: Elements of Finite Model Theory. Springer, New York (2004)

    Book  MATH  Google Scholar 

  16. Meredith, P., Rosu, G.: Efficient parametric runtime verification with deterministic string rewriting. In: 2013 IEEE/ACM 28th International Conference on Automated Software Engineering (ASE), pp. 70–80. IEEE (2013)

    Google Scholar 

  17. Navabpour, S., Joshi, Y., Wu, W., Berkovich, S., Medhat, R., Bonakdarpour, B., Fischmeister, S.: RiTHM: a tool for enabling time-triggered runtime verification for C programs. In: ACM Symposium on the Foundations of Software Engineering (FSE), pp. 603–606 (2013)

    Google Scholar 

  18. Sokolsky, O., Sammapun, U., Lee, I., Kim, J.: Run-time checking of dynamic properties. Electron. Notes Theoret. Comput. Sci. 144(4), 91–108 (2006)

    Article  Google Scholar 

  19. Williams, M.: Scaling Web Applications with NGINX, Part II: Caching and Monitoring (2015). https://www.nginx.com/blog/. Accessed 27 May 2016

  20. Zink, M., Suh, K., Gu, Y., Kurose, J.: Watch global, cache local: Youtube network traffic at a campus network: measurements and implications. In: Electronic Imaging 2008, p. 681805. International Society for Optics and Photonics (2008)

    Google Scholar 

Download references

Acknowledgments

This work was partially sponsored by Canada NSERC Discovery Grant 418396-2012 and NSERC Strategic Grants 430575-2012 and 463324-2014.

Author information

Authors and Affiliations

  1. McMaster University, Hamilton, Canada

    Borzoo Bonakdarpour

  2. University of Waterloo, Waterloo, Canada

    Ramy Medhat, Sebastian Fischmeister & Yogi Joshi

Authors
  1. Ramy Medhat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sebastian Fischmeister
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yogi Joshi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ramy Medhat .

Editor information

Editors and Affiliations

  1. Université Grenoble Alpes, Inria, Grenoble, France

    Yliès Falcone

  2. IMDEA Software Institute, Madrid, Spain

    César Sánchez

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Medhat, R., Bonakdarpour, B., Fischmeister, S., Joshi, Y. (2016). Accelerated Runtime Verification of LTL Specifications with Counting Semantics. In: Falcone, Y., Sánchez, C. (eds) Runtime Verification. RV 2016. Lecture Notes in Computer Science(), vol 10012. Springer, Cham. https://doi.org/10.1007/978-3-319-46982-9_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46982-9_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46981-2

  • Online ISBN: 978-3-319-46982-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation