Skip to main content
SpringerLink
Log in

A Foundation for Runtime Monitoring

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

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

Included in the following conference series:

Abstract

Runtime Verification is a lightweight technique that complements other verification methods in an effort to ensure software correctness. The technique poses novel questions to software engineers: it is not easy to identify which specifications are amenable to runtime monitoring, nor is it clear which monitors effect the required runtime analysis correctly. This exposition targets a foundational understanding of these questions. Particularly, it considers an expressive specification logic (a syntactic variant of the modal \(\mu \)-calculus) that is agnostic of the verification method used, together with an elemental framework providing an operational semantics for the runtime analysis performed by monitors. The correspondence between the property satisfactions in the logic on the one hand, and the verdicts reached by the monitors performing the analysis on the other, is a central theme of the study. Such a correspondence underpins the concept of monitorability, used to identify the subsets of the logic that can be adequately monitored for by RV. Another theme of the study is that of understanding what should be expected of a monitor in order for the verification process to be correct. We show how the monitor framework considered can constitute a basis whereby various notions of monitor correctness may be defined and investigated.

This work was supported by the project “TheoFoMon: Theoretical Foundations for Monitorability” (nr.163406-051) of the Icelandic Research Fund and the Marie Curie INDAM-COFUND-2012 Outgoing Fellowship.

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.

    This may be due to event knowledge gaps from the instrumentation-side or knowledge disagreements between the monitors and the instrumentation [11].

References

  1. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: On the complexity of determinizing monitors. In: Carayol, A., Nicaud, C. (eds.) CIAA 2017. LNCS, vol. 10329, pp. 1–13. Springer, Cham (2017). doi:10.1007/978-3-319-60134-2_1

    Chapter  Google Scholar 

  2. Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007)

    Book  MATH  Google Scholar 

  3. Ahrendt, W., Chimento, J.M., Pace, G.J., Schneider, G.: A specification language for static and runtime verification of data and control properties. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 108–125. Springer, Cham (2015). doi:10.1007/978-3-319-19249-9_8

    Chapter  Google Scholar 

  4. Aktug, I., Naliuka, K.: ConSpec - a formal language for policy specification. Sci. Comput. Program. 74(1–2), 2–12 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  5. Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M.R., Pasareanu, C.S., Rosu, G., Sen, K., Visser, W., Washington, R.: Combining test case generation and runtime verification. Theor. Comput. Sci. 336(2–3), 209–234 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  6. Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473–481. Springer, Cham (2016). doi:10.1007/978-3-319-46982-9_31

    Chapter  Google Scholar 

  7. Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: SEFM, LNCS (2017, to appear)

    Google Scholar 

  8. Azzopardi, S., Colombo, C., Pace, G.J., Vella, B.: Compliance checking in the open payments ecosystem. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 337–343. Springer, Cham (2016). doi:10.1007/978-3-319-41591-8_23

    Google Scholar 

  9. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, New York (2008)

    MATH  Google Scholar 

  10. Barringer, H., Goldberg, A., Havelund, K., Sen, K.: Rule-based runtime verification. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 44–57. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24622-0_5

    Chapter  Google Scholar 

  11. Basin, D., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring compliance policies over incomplete and disagreeing logs. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 151–167. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35632-2_17

    Chapter  Google Scholar 

  12. Brat, G.P., Drusinsky, D., Giannakopoulou, D., Goldberg, A., Havelund, K., Lowry, M.R., Pasareanu, C.S., Venet, A., Visser, W., Washington, R.: Experimental evaluation of verification and validation tools on martian rover software. Formal Methods Syst. Des. 25(2–3), 167–198 (2004)

    Article  MATH  Google Scholar 

  13. Cassar, I., Francalanza, A.: Runtime adaptation for actor systems. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 38–54. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_3

    Chapter  Google Scholar 

  14. Cassar, I., Francalanza, A.: On implementing a monitor-oriented programming framework for actor systems. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 176–192. Springer, Cham (2016). doi:10.1007/978-3-319-33693-0_12

    Chapter  Google Scholar 

  15. Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: eAOP - an aspect oriented programming framework for erlang. In: Erlang Workshop (2017, to appear)

    Google Scholar 

  16. Chen, F., Rosu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588 (2007)

    Google Scholar 

  17. Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  18. Colombo, C., Francalanza, A., Mizzi, R., Pace, G.J.: polyLarva: runtime verification with configurable resource-aware monitoring boundaries. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 218–232. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33826-7_15

    Chapter  Google Scholar 

  19. D’Angelo, B., Sankaranarayanan, S., Sánchez, C., Robinson, W., Finkbeiner, B., Sipma, H.B., Mehrotra, S., Manna, Z.: LOLA: runtime monitoring of synchronous systems. In: TIME, pp. 166–174 (2005)

    Google Scholar 

  20. Debois, S., Hildebrandt, T., Slaats, T.: Safety, liveness and run-time refinement for modular process-aware information systems with dynamic sub processes. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 143–160. Springer, Cham (2015). doi:10.1007/978-3-319-19249-9_10

    Chapter  Google Scholar 

  21. Decker, N., Leucker, M., Thoma, D.: jUnitRV–adding runtime verification to jUnit. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 459–464. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38088-4_34

    Chapter  Google Scholar 

  22. Monica, D.D., Francalanza, A.: Towards a hybrid approach to software verification. In: NWPT, number SCS16001 in RUTR, pp. 51–54 (2015)

    Google Scholar 

  23. Francalanza, A.: A theory of monitors. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 145–161. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49630-5_9

    Chapter  Google Scholar 

  24. Francalanza, A.: Consistently-detecting monitors. In: CONCUR. Dagstuhl Publishing (LIPICS) (2017)

    Google Scholar 

  25. Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying hennessy-milner logic with recursion at runtime. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 71–86. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_5

    Chapter  Google Scholar 

  26. Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the hennessy-milner logic with recursion. Formal Methods Syst. Des., 1–30 (2017)

    Google Scholar 

  27. Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Methods Syst. Des. 46(3), 226–261 (2015)

    Article  MATH  Google Scholar 

  28. Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_7

    Chapter  Google Scholar 

  29. Kassem, A., Falcone, Y., Lafourcade, P.: Monitoring electronic exams. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 118–135. Springer, Cham (2015). doi:10.1007/978-3-319-23820-3_8

    Chapter  Google Scholar 

  30. Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: a run-time assurance approach for Java programs. Formal Methods Syst. Des. 24(2), 129–155 (2004)

    Article  MATH  Google Scholar 

  31. Klamka, J.: system characteristics: stability, controllability, observability. In: Control System, Robotics and Automation, EOLLS, vol. 7 (2009)

    Google Scholar 

  32. Kozen, D.: Results on the propositional \(\upmu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  33. Larsen, K.G.: Proof systems for satisfiability in hennessy-milner logic with recursion. Theor. Comput. Sci. 72(2&3), 265–288 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  34. Lerda, F., Visser, W.: Addressing dynamic issues of program model checking. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 80–102. Springer, Heidelberg (2001). doi:10.1007/3-540-45139-0_6

    Chapter  Google Scholar 

  35. Leucker, M., Schallhart, C.: A brief account of runtime verification. J. Log. Algebr. Program. 78(5), 293–303 (2009)

    Article  MATH  Google Scholar 

  36. Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Secur. 4(1–2), 2–16 (2005)

    Article  Google Scholar 

  37. Meredith, P.O., Jin, D., Griffith, D., Chen, F., Rosu, G.: An overview of the MOP runtime verification framework. STTT 14(3), 249–289 (2012)

    Article  Google Scholar 

  38. Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: CC, pp. 98–108 (2017)

    Google Scholar 

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

  40. Varvaressos, S., Vaillancourt, D., Gaboury, S., Blondin Massé, A., Hallé, S.: Runtime monitoring of temporal logic properties in a platform game. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 346–351. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40787-1_23

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Malta, Msida, Malta

    Adrian Francalanza, Duncan Paul Attard & Ian Cassar

  2. School of Computer Science, Reykjavík University, Reykjavik, Iceland

    Luca Aceto, Antonis Achilleos, Duncan Paul Attard, Ian Cassar & Anna Ingólfsdóttir

  3. Departamento de Sistemas Informáticos y Computación, Universidad Complutense de Madrid, Madrid, Spain

    Dario Della Monica

  4. Dipartimento di Ingegneria Elettrica e Tecnologie dell’Informazione, Università “Federico II” di Napoli, Naples, Italy

    Dario Della Monica

Authors
  1. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Aceto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Antonis Achilleos
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Duncan Paul Attard
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ian Cassar
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Dario Della Monica
    View author publications

    You can also search for this author in PubMed Google Scholar

  7. Anna Ingólfsdóttir
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Adrian Francalanza .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Francalanza, A. et al. (2017). A Foundation for Runtime Monitoring. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation