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.
Chapter PDF
Similar content being viewed by others
Keywords
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
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)
Avgustinov, P., Tibble, J., de Moor, O.: Making trace monitors feasible. SIGPLAN Not. 42(10), 589–608 (2007)
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)
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)
Basin, D.: Monpoly: Monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) Runtime Verification. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012)
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)
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)
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)
Cruz, H.C.: Optimisation techniques for runtime verification. Master’s thesis, University of Manchester (2014)
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)
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)
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)
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)
Jin, D., Meredith, P.O., Griffith, D., Rosu, G.: Garbage collection for monitoring parametric properties. SIGPLAN Not. 46(6), 415–424 (2011)
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)
Leucker, M., Schallhart, C.: A brief account of runtime verification. Journal of Logic and Algebraic Programming 78(5), 293–303 (2008)
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)
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)
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)
Reger, G.: Automata Based Monitoring and Mining of Execution Traces. PhD thesis, University of Manchester (2014)
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)
Roşu, G., Chen, F.: Semantics and algorithms for parametric monitoring. TACAS 2009 8(1), 1–47 (2012); Short version presented at TACAS 2009
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Reger, G., Cruz, H.C., Rydeheard, D. (2015). MarQ: Monitoring at Runtime with QEA. In: Baier, C., Tinelli, C. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2015. Lecture Notes in Computer Science(), vol 9035. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46681-0_55
Download citation
DOI: https://doi.org/10.1007/978-3-662-46681-0_55
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46680-3
Online ISBN: 978-3-662-46681-0
eBook Packages: Computer ScienceComputer Science (R0)