Skip to main content
SpringerLink
Log in

From First-order Temporal Logic to Parametric Trace Slicing

  • Conference paper
  • First Online:
Runtime Verification

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

Abstract

Parametric runtime verification is the process of verifying properties of execution traces of (data carrying) events produced by a running system. This paper considers the relationship between two widely-used specification approaches to parametric runtime verification: trace slicing and first-order temporal logic. This work is a first step in understanding this relationship. We introduce a technique of identifying syntactic fragments of temporal logics that admit notions of sliceability. We show how to translate formulas in such fragments into automata with a slicing-based semantics. In exploring this relationship, the paper aims to allow monitoring techniques to be shared between the two approaches and initiate a wider effort to unify specification languages for runtime verification.

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

Notes

  1. 1.

    Here we refer to the notion of slicing in Sect. 3. A more general notion of slicing involves free variables [3], which could be used for y. It is future work to consider this generalisation.

References

  1. CSRV 2014. http://rv2014.imag.fr/monitoring-competition

  2. Allan, C., Avgustinov, P., Christensen, A.S., Hendren, L., Kuzins, S., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: Adding trace matching with free variables to AspectJ. SIGPLAN Not. 40, 345–364 (2005)

    Article  MATH  Google Scholar 

  3. Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.: Quantified event automata: towards expressive and efficient runtime monitors. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 68–84. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from EAGLE to RuleR. J. Logic Comput. 20(3), 675–706 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  5. Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  6. Bauer, A., Falcone, Y.: Decentralised LTL monitoring. CoRR, abs/1111.5133 (2011)

    Google Scholar 

  7. Bauer, A., Küster, J.-C., Vegliach, G.: The ins and outs of first-order runtime verification. Formal Methods in Syst. Des., 46, 1–31 (2015)

    Google Scholar 

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

    Article  MathSciNet  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. 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 

  11. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM (1999)

    Google Scholar 

  12. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. IOS Press, Amsterdam (2013)

    Google Scholar 

  13. Lee, C., Jin, D., Meredith, P.O., Roşu, G.: Towards categorizing and formalizing the JDK API. Technical report. Department of Computer Science, University of Illinois at Urbana-Champaign (2012). http://hdl.handle.net/2142/30006

  14. Medhat, R., Joshi, Y., Bonakdarpour, B., Fischmeister, S.: Parallelized runtime verification of first-order LTL specifications. Technical report, University of Waterloo (2014)

    Google Scholar 

  15. Meredith, P., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. J. Softw. Tools Technol. Transfer 14(3), 249–289 (2011)

    Article  Google Scholar 

  16. Reger, G.: Automata based monitoring and mining of execution traces. Ph.D. thesis, University of Manchester (2014)

    Google Scholar 

  17. Reger, G., Cruz, H.C., Rydeheard, D.: 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) (2015)

    Google Scholar 

  18. Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)

    Article  Google Scholar 

  19. Shen, Y., Li, J., Wang, Z., Su, T., Fang, B., Pu, G., Liu, W.: Runtime verification by convergent formula progression. In: APSEC 2014 (2014)

    Google Scholar 

  20. Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proceedings of the 5th International Workshop on Runtime Verification (RV 2005). ENTCS, vol. 144(4), pp. 109–124. Elsevier (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, Manchester, UK

    Giles Reger & David Rydeheard

Authors
  1. Giles Reger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David Rydeheard
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Giles Reger .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Max Planck Institute for Software Systems, Kaiserslautern, Germany

    Rupak Majumdar

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Reger, G., Rydeheard, D. (2015). From First-order Temporal Logic to Parametric Trace Slicing. In: Bartocci, E., Majumdar, R. (eds) Runtime Verification. Lecture Notes in Computer Science(), vol 9333. Springer, Cham. https://doi.org/10.1007/978-3-319-23820-3_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23820-3_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23819-7

  • Online ISBN: 978-3-319-23820-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation