Skip to main content
SpringerLink
Log in

An Overview of MarQ

  • 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

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.

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.

    See http://rv2014.imag.fr/monitoring-competition/results.html.

  2. 2.

    See https://www.cost-arvi.eu/?page_id=664.

References

  1. 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

    Chapter  Google Scholar 

  2. 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

    Chapter  Google Scholar 

  3. 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)

    Google Scholar 

  4. 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

    Chapter  Google Scholar 

  5. Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Transf. (STTT) 17(2), 143–170 (2014)

    Article  Google Scholar 

  6. 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

    Google Scholar 

  7. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebraic Program. 78(5), 293–303 (2008)

    Article  MATH  Google Scholar 

  8. 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)

    Google Scholar 

  9. Reger, G.: Automata based monitoring and mining of execution traces. PhD thesis, University of Manchester (2014)

    Google Scholar 

  10. 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

    Chapter  Google Scholar 

  11. 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

    Google Scholar 

  12. 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

    Google Scholar 

  13. 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)

    Google Scholar 

  14. 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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Manchester, Manchester, UK

    Giles Reger

Authors
  1. Giles Reger
    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. 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

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)

Publish with us

Policies and ethics

Search

Navigation