Advertisement

Abstract

Runtime monitoring is the process of checking whether an execution trace of a running system satisfies a given specification. For this to be effective, monitors which run trace-checking algorithms must be efficient so that they introduce minimal computational overhead. We present the MarQ tool for monitoring properties expressed as Quantified Event Automata. This formalism generalises previous automata-based specification methods. MarQ extends the established parametric trace slicing technique and incorporates existing techniques for indexing and garbage collection as well as a new technique for optimising runtime monitoring: structural specialisations where monitors are generated based on structural characteristics of the monitored property. MarQ recently came top in two tracks in the 1st international Runtime Verification competition, showing that MarQ is one of the most efficient existing monitoring tools for both offline monitoring of trace logs and online monitoring of running systems.

Keywords

Free Variable Garbage Collection Online Monitoring Execution Trace Concrete Event 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
  2. 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)CrossRefGoogle Scholar
  3. 3.
    Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. SIGPLAN Not. 42(10), 589–608 (2007)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Bartocci, E., Bonakdarpour, B., Falcone, Y.: First international competition on software for runtime verification. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 1–9. Springer, Heidelberg (2014)CrossRefGoogle Scholar
  6. 6.
    Basin, D.: Monpoly: Monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) Runtime Verification. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    Bauer, A., Leucker, M., Schallhart, C.: The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 126–138. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    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)CrossRefGoogle Scholar
  9. 9.
    Colombo, C., Pace, G.J., Schneider, G.: Larva — safer monitoring of real-time java programs (tool paper). In: Proceedings of the 2009 Seventh IEEE International Conference on Software Engineering and Formal Methods, SEFM 2009, pp. 33–37. IEEE Computer Society, Washington, DC (2009)CrossRefGoogle Scholar
  10. 10.
    Cruz, H.C.: Optimisation techniques for runtime verification. Master’s thesis, University of Manchester (2014)Google Scholar
  11. 11.
    D’Angelo, B., Sankaranarayanan, S., Sanchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: Lola: Runtime monitoring of synchronous systems. In: 2013 20th International Symposium on Temporal Representation and Reasoning, pp. 166–174 (2005)Google Scholar
  12. 12.
    Decker, N., Leucker, M., Thoma, D.: Junitrv–adding runtime verification to junit. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods. LNCS, vol. 7871, pp. 459–464. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 341–356. Springer, Heidelberg (2014)Google Scholar
  14. 14.
    Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D. (eds.) Summer School Marktoberdorf 2012 - Engineering Dependable Software Systems. IOS Press (2013) (to appear)Google Scholar
  15. 15.
    Jin, D., Meredith, P.O., Griffith, D., Rosu, G.: Garbage collection for monitoring parametric properties. SIGPLAN Not. 46(6), 415–424 (2011)CrossRefGoogle Scholar
  16. 16.
    Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of aspectj. In: Lindskov Knudsen, J. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  17. 17.
    Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2008)CrossRefGoogle Scholar
  18. 18.
    Meredith, P., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the mop runtime verification framework. J. Software Tools for Technology Transfer, 1–41 (2011)Google Scholar
  19. 19.
    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: Proceedings of the, 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE, pp. 603–606. ACM, New York (2013)Google Scholar
  20. 20.
    Purandare, R., Dwyer, M.B., Elbaum, S.: Monitoring finite state properties: Algorithmic approaches and their relative strengths. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 381–395. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  21. 21.
    Reger, G.: Automata Based Monitoring and Mining of Execution Traces. PhD thesis, University of Manchester (2014)Google Scholar
  22. 22.
    Reger, G., Barringer, H., Rydeheard, D.: A pattern-based approach to parametric specification mining. In: Proceedings of the 28th IEEE/ACM International Conference on Automated Software Engineering (November 2013) (to appear)Google Scholar
  23. 23.
    Roşu, G., Chen, F.: Semantics and algorithms for parametric monitoring. TACAS 2009 8(1), 1–47 (2012); Short version presented at TACAS 2009Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2015

Authors and Affiliations

  • Giles Reger
    • 1
  • Helena Cuenca Cruz
    • 1
  • David Rydeheard
    • 1
  1. 1.University of ManchesterManchesterUK

Personalised recommendations