Abstract
MarQ is a runtime monitoring tool for specifications written as quantified event automata, an expressive automata-based specification language based on the notion of parametric trace slicing. MarQ has performed well in the runtime verification competition and implements advanced indexing and redundancy elimination techniques. This overview describes the basic structure and functionality provided by MarQ and gives a brief description of how to use the tool.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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). doi:10.1007/978-3-642-32759-9_9
Decker, N., Harder, J., Scheffel, T., Schmitz, M., Thoma, D.: Runtime monitoring with union-find structures. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 868–884. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_54
Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D. (eds.) Summer School Marktoberdorf - Engineering Dependable Software Systems (2012). IOS Press (2013, To appear)
Falcone, Y., Nickovic, D., Reger, G., Thoma, D.: Second international competition on runtime verification. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 405–422. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_27
Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. (STTT) 17(2), 143–170 (2014)
Havelund, K., Reger, G.: Formal modeling and verification of cyber-physical systems. In: Drechsler, R., Kühne, U. (eds.) Specification of parametric monitors. Springer, Wiesbaden (2015). doi:10.1007/978-3-658-09994-7_6
Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 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. Softw. Tools Technol. Transf. 1–41 (2011)
Reger, G.: Automata based monitoring and mining of execution traces. PhD thesis, University of Manchester (2014)
Reger, G.: Suggesting edits to explain failing traces. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 287–293. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_20
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
Reger, G., Cruz, H.C., Rydeheard, D.: MarQ: monitoring at runtime with QEA. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 596–610. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_55
Reger, G., Hallé, S., Falcone, Y.: Third international competition on runtime verification CRV. In: Falcone, Y., Sánchez, C. (eds.) Runtime Verification - 16th International Conference. RV 2016. LNCS, pp. 21–37, Springer, Switzerland (2016, to appear)
Reger, G., Rydeheard, D.: From first-order temporal logic to parametric trace slicing. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 216–232. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_14
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Reger, G. (2016). An Overview of MarQ . 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_34
Download citation
DOI: https://doi.org/10.1007/978-3-319-46982-9_34
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)