Skip to main content
SpringerLink
Log in

Introduction to Runtime Verification

  • Chapter
  • First Online:
Lectures on Runtime Verification

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

Abstract

The aim of this chapter is to act as a primer for those wanting to learn about Runtime Verification (RV). We start by providing an overview of the main specification languages used for RV. We then introduce the standard terminology necessary to describe the monitoring problem, covering the pragmatic issues of monitoring and instrumentation, and discussing extensively the monitorability problem.

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 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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

References

  1. Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: Monitoring for silent actions. In: FSTTCS. LIPIcs, vol. 93, pp. 43:1–43:14 (2017, to appear)

    Google Scholar 

  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(10), 345–364 (2005)

    Article  MATH  Google Scholar 

  3. Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_35

    Chapter  Google Scholar 

  4. Amiar, A., Delahaye, M., Falcone, Y., du Bousquet, L.: Compressing microcontroller execution traces to assist system analysis. In: Schirner, G., Götz, M., Rettberg, A., Zanella, M.C., Rammig, F.J. (eds.) IESS 2013. IAICT, vol. 403, pp. 139–150. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38853-8_13

    Chapter  Google Scholar 

  5. Amiar, A., Delahaye, M., Falcone, Y., du Bousquet, L.: Fault localization in embedded software based on a single cyclic trace. In: IEEE 24th International Symposium on Software Reliability Engineering, ISSRE 2013, Pasadena, CA, USA, 4–7 November 2013, pp. 148–157. IEEE Computer Society (2013)

    Google Scholar 

  6. Arnold, M., Vechev, M.T., Yahav, E.: QVM: an efficient runtime for detecting defects in deployed systems. In: Proceedings of OOPSLA 2008: The 23rd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, pp. 143–162. ACM (2008)

    Google Scholar 

  7. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49, 2002 (2001)

    MathSciNet  MATH  Google Scholar 

  8. 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). https://doi.org/10.1007/978-3-319-46982-9_31

    Chapter  Google Scholar 

  9. Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 219–235. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66197-1_14

    Chapter  Google Scholar 

  10. Avgustinov, P., Christensen, A.S., Hendren, L.J., Kuzins, S., Lhoták, J., Lhoták, O., de Moor, O., Sereni, D., Sittampalam, G., Tibble, J.: abc: an extensible AspectJ compiler. Trans. Aspect-Oriented Softw. Dev. I 3880(3880), 293–334 (2006)

    Article  MATH  Google Scholar 

  11. Baader, F., Bauer, A., Lippmann, M.: Runtime verification using a temporal description logic. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS (LNAI), vol. 5749, pp. 149–164. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04222-5_9

    Chapter  Google Scholar 

  12. 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). https://doi.org/10.1007/978-3-642-32759-9_9

    Chapter  Google Scholar 

  13. Barringer, H., Goldberg, A., Havelund, K., Sen, K.:. Program monitoring with LTL in EAGLE. In: 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), Abstracts Proceedings, 26–30 April 2004, Santa Fe, New Mexico, USA (2004)

    Google Scholar 

  14. 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). https://doi.org/10.1007/978-3-540-24622-0_5

    Chapter  Google Scholar 

  15. Barringer, H., Havelund, K.: TraceContract: a scala DSL for trace analysis. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 57–72. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_7

    Chapter  Google Scholar 

  16. Barringer, H., Rydeheard, D.E., Havelund, K.: Rule systems for run-time monitoring: from Eagle to RuleR. J. Log. Comput. 20(3), 675–706 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  17. 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, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_1

    Google Scholar 

  18. Bartocci, E., Bortolussi, L., Loreti, M., Nenzi, L.: Monitoring mobile and spatially distributed cyber-physical systems. In: Proceedings of MEMOCODE 2017: The 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, pp. 146–155. ACM (2017)

    Google Scholar 

  19. Bartocci, E., Bortolussi, L., Milios, D., Nenzi, L., Sanguinetti, G.: Studying emergent behaviours in morphogenesis using signal spatio-temporal logic. In: Abate, A., Šafránek, D. (eds.) HSB 2015. LNCS, vol. 9271, pp. 156–172. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26916-0_9

    Chapter  Google Scholar 

  20. Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Model checking biological oscillators. Electr. Notes Theor. Comput. Sci. 229(1), 41–58 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  21. Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Detecting synchronisation of biological oscillators by model checking. Theor. Comput. Sci. 411(20), 1999–2018 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  22. Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 135–175. Springer, Cham (2018)

    Chapter  Google Scholar 

  23. Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., Rosu, G., Signoles, J., Thoma, D., Zalinescu, E., Zhang, Y.: First international competition on runtime verification: rules, benchmarks, tools, and final results of CRV 2014. Int. J. Softw. Tools Technol. Transf. (2017)

    Google Scholar 

  24. Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168–182. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_18

    Chapter  Google Scholar 

  25. Basin, D.A., Klaedtke, F., Müller, S., Zalinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15:1–15:45 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  26. Basin, D., Klaedtke, F., Zălinescu, E.: Runtime verification of temporal properties over out-of-order data streams. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 356–376. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_18

    Chapter  Google Scholar 

  27. Basin, D., Krstić, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 85–102. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_6

    Chapter  Google Scholar 

  28. Bauer, A., Küster, J.-C., Vegliach, G.: The ins and outs of first-order runtime verification. Form. Methods Syst. Des. 46(3), 286–316 (2015)

    Article  MATH  Google Scholar 

  29. 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). https://doi.org/10.1007/978-3-540-77395-5_11

    Chapter  Google Scholar 

  30. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), 14:1–14:64 (2011)

    Article  Google Scholar 

  31. Bauer, A., Leucker, M., Streit, J.: SALT—structured assertion language for temporal logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 757–775. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_41

    Chapter  Google Scholar 

  32. Bauer, A.K., Falcone, Y.: Decentralised LTL monitoring. Form. Methods Syst. Des. 48(1–2), 49–93 (2016)

    MATH  Google Scholar 

  33. Berkovich, S., Bonakdarpour, B., Fischmeister, S.: Runtime verification with minimal intrusion through parallelism. Form. Methods Syst. Des. 46(3), 317–348 (2015)

    Article  MATH  Google Scholar 

  34. Bernat, A.R., Miller, B.P.: Anywhere, any-time binary instrumentation. In: Proceedings of PASTE 2011: The 10th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools, pp. 9–16. ACM (2011)

    Google Scholar 

  35. Bielova, N., Massacci, F.: Do you really mean what you actually enforced?: edited automata revisited. Int. J. Inf. Secur. 10(4), 239–254 (2011)

    Article  Google Scholar 

  36. Bodden, E., Havelund, K.: Racer: effective race detection using AspectJ. In: Proceedings of ISSTA 2008: The 2008 International Symposium on Software Testing and Analysis, ISSTA 2008, pp. 155–166. ACM (2008)

    Google Scholar 

  37. Bollig, B., Decker, N., Leucker, M.: Frequency linear-time temporal logic. In: Proceedings of the 6th International Symposium on Theoretical Aspects of Software Engineering (TASE 2012), Beijing, China, pp. 85–92. IEEE Computer Society Press (2012)

    Google Scholar 

  38. Bonakdarpour, B., Navabpour, S., Fischmeister, S.: Sampling-based runtime verification. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 88–102. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_9

    Chapter  Google Scholar 

  39. Bonér, J.: What are the key issues for commercial AOP use: how does AspectWerkz address them? In: Proceedings of the 3rd International Conference on Aspect-Oriented Software Development, AOSD 2004, Lancaster, UK, 22–24 March 2004, pp. 5–6. ACM (2004)

    Google Scholar 

  40. Bruening, D., Garnett, T., Amarasinghe, S.P.: An infrastructure for adaptive dynamic optimization. In: Proceedings of CGO 2003: The 1st IEEE/ACM International Symposium on Code Generation and Optimization, pp. 265–275. IEEE Computer Society (2003)

    Google Scholar 

  41. Bultan, T., Sen, K. (eds.): Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM, New York (2017)

    Google Scholar 

  42. Calafato, A., Colombo, C., Pace, G.J.: A controlled natural language for tax fraud detection. In: Davis, B., Pace, G.J.J., Wyner, A. (eds.) CNL 2016. LNCS (LNAI), vol. 9767, pp. 1–12. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41498-0_1

    Chapter  Google Scholar 

  43. Calder, M., Sevegnani, M.: Process algebra for event-driven runtime verification: a case study of wireless network management. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 21–23. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_2

    Chapter  Google Scholar 

  44. Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor-based systems. In: Proceedings 13th International Workshop on Foundations of Coordination Languages and Self-Adaptive Systems. Electronic Proceedings in Theoretical Computer Science, Rome, Italy, 6th September 2014, vol. 175, pp. 54–68. Open Publishing Association (2015)

    Google Scholar 

  45. 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). https://doi.org/10.1007/978-3-319-23820-3_3

    Chapter  Google Scholar 

  46. 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). https://doi.org/10.1007/978-3-319-33693-0_12

    Chapter  Google Scholar 

  47. Cassar, I., Francalanza, A., Aceto, L., Ingólfsdóttir, A.: A survey of runtime monitoring instrumentation techniques. In: PrePost@iFM. EPTCS, vol. 254, pp. 15–28 (2017)

    Google Scholar 

  48. Cau, A., Zedan, H.: Refining interval temporal logic specifications. In: Bertran, M., Rus, T. (eds.) ARTS 1997. LNCS, vol. 1231, pp. 79–94. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63010-4_6

    Chapter  Google Scholar 

  49. Chen, F., Roşu, G.: Towards monitoring-oriented programming: a paradigm combining specification and implementation. In: ENTCS, pp. 106–125. Elsevier (2003)

    Google Scholar 

  50. Chen, F., Roşu, G.: Java-MOP: a monitoring oriented programming environment for Java. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 546–550. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_36

    Chapter  Google Scholar 

  51. Chen, F., Roşu, G.: MOP: an efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588. ACM Press (2007)

    Google Scholar 

  52. 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). https://doi.org/10.1007/978-3-642-00768-2_23

    Chapter  Google Scholar 

  53. Chomicki, J.: Efficient checking of temporal integrity constraints using bounded history encoding. ACM Trans. Database Syst. 20(2), 149–186 (1995)

    Article  Google Scholar 

  54. Cini, C., Francalanza, A.: An LTL proof system for runtime verification. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 581–595. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_54

    Google Scholar 

  55. Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15

    Chapter  Google Scholar 

  56. Colombo, C., Falcone, Y.: Organising LTL monitors over distributed systems with a global clock. Form. Methods Syst. Des. 49(1–2), 109–158 (2016)

    Article  Google Scholar 

  57. 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). https://doi.org/10.1007/978-3-642-33826-7_15

    Chapter  Google Scholar 

  58. Colombo, C., Pace, G.J.: Industrial experiences with runtime verification of financial transaction systems: lessons learnt and standing challenges. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 211–232. Springer, Cham (2018)

    Chapter  Google Scholar 

  59. Colombo, C., Pace, G.J., Schneider, G.: LARVA – safer monitoring of real-time java programs (tool paper). In: Proceedings of SEFM 2009: The Seventh IEEE International Conference on Software Engineering and Formal Methods, pp. 33–37. IEEE Computer Society (2009)

    Google Scholar 

  60. Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Self-adaptive monitors for multiparty sessions. In: PDP, pp. 688–696. IEEE Computer Society (2014)

    Google Scholar 

  61. Daian, P., Falcone, Y., Meredith, P., Şerbănuţă, T.F., Shiriashi, S., Iwai, A., Rosu, G.: RV-Android: efficient parametric android runtime verification, a brief tutorial. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 342–357. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_24

    Chapter  Google Scholar 

  62. De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence, IJCAI 2013, pp. 854–860. AAAI Press (2013)

    Google Scholar 

  63. Decker, N., Gottschling, P., Hochberger, C., Leucker, M., Scheffel, T., Schmitz, M., Weiss, A.: Rapidly adjustable non-intrusive online monitoring for multi-core systems. In: Cavalheiro, S., Fiadeiro, J. (eds.) SBMF 2017. LNCS, vol. 10623, pp. 179–196. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70848-5_12

    Chapter  Google Scholar 

  64. Decker, N., Thoma, D.: On freeze LTL with ordered attributes. In: Jacobs, B., Löding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 269–284. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49630-5_16

    Chapter  Google Scholar 

  65. Diekert, V., Leucker, M.: Topology, monitorable properties and runtime verification. Theor. Comput. Sci. 537, 29–41 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  66. Diekert, V., Muscholl, A., Walukiewicz, I.: A note on monitors and Büchi automata. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 39–57. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_3

    Chapter  Google Scholar 

  67. El-Harake, K., Falcone, Y., Jerad, W., Langet, M., Mamlouk, M.: Blocking advertisements on android devices using monitoring techniques. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 239–253. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45231-8_17

    Google Scholar 

  68. El-Hokayem, A., Falcone, Y.: Monitoring decentralized specifications. In: Bultan and Sen [41], pp. 125–135

    Google Scholar 

  69. El-Hokayem, A., Falcone, Y.: THEMIS: a tool for decentralized monitoring algorithms. In: Bultan and Sen [41], pp. 372–375

    Google Scholar 

  70. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 995–1072. MIT Press, Cambridge (1990)

    Google Scholar 

  71. Erlingsson, U.: The inlined reference monitor approach to security policy enforcement. Ph.D. thesis, Cornell University (2004)

    Google Scholar 

  72. 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, Amsterdam (2013)

    Google Scholar 

  73. Falcone, Y., Currea, S.: Weave droid: aspect-oriented programming on android devices: fully embedded or in the cloud. In: Goedicke, M., Menzies, T., Saeki, M. (eds.) IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, Essen, Germany, 3–7 September 2012, pp. 350–353. ACM (2012)

    Google Scholar 

  74. Falcone, Y., Currea, S., Jaber, M.: Runtime verification and enforcement for Android applications with RV-Droid. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 88–95. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_11

    Chapter  Google Scholar 

  75. Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40–59. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04694-0_4

    Chapter  Google Scholar 

  76. Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)

    Article  Google Scholar 

  77. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D.A., Kalus, G. (eds.) Engineering Dependable Software Systems. NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 34, pp. 141–175. IOS Press, Amsterdam (2013)

    Google Scholar 

  78. Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 204–220. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_15

    Chapter  Google Scholar 

  79. Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14(1), 173–199 (2015)

    Article  Google Scholar 

  80. Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018)

    Chapter  Google Scholar 

  81. Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form. Methods Syst. Des. 38(3), 223–262 (2011)

    Article  MATH  Google Scholar 

  82. Faymonville, P., Finkbeiner, B., Schirmer, S., Torfah, H.: A stream-based specification language for network monitoring. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 152–168. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_10

    Chapter  Google Scholar 

  83. Fei, L., Midkiff, S.P.: Artemis: practical runtime monitoring of applications for execution anomalies. In: Proceedings of the ACM SIGPLAN 2006: Conference on Programming Language Design and Implementation, pp. 84–95. ACM (2006)

    Google Scholar 

  84. Fischmeister, S., Lam, P.: On time-aware instrumentation of programs. In: Proceedings of the 2009 15th IEEE Symposium on Real-Time and Embedded Technology and Applications, RTAS 2009, pp. 305–314. IEEE Computer Society, Washington, DC (2009)

    Google Scholar 

  85. Foster, H.Q., Marschner, E., Wolfsthal, Y.: IEEE 1850 PSL: The Next Generation (2005)

    Google Scholar 

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

    Chapter  Google Scholar 

  87. Francalanza, A.: Consistently-detecting monitors. In: CONCUR. LIPIcs, vol. 85, pp. 8:1–8:19 (2017)

    Google Scholar 

  88. Francalanza, A., Aceto, L., Achilleos, A., Attard, D.P., Cassar, I., Della Monica, D., Ingólfsdóttir, A.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 8–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_2

    Chapter  Google Scholar 

  89. 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). https://doi.org/10.1007/978-3-319-23820-3_5

    Chapter  Google Scholar 

  90. Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy-Milner logic with recursion. J. Form. Methods Syst. Des. (FMSD) 51(1), 87–116 (2017)

    Article  MATH  Google Scholar 

  91. Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5–7), 186–215 (2013)

    MathSciNet  MATH  Google Scholar 

  92. Francalanza, A., Perez, J.A., Sanchez, C.: Runtime verification for decentralized and distributed systems. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 176–210. Springer, Cham (2018)

    Chapter  Google Scholar 

  93. Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. FMSD 46(3), 226–261 (2015)

    MATH  Google Scholar 

  94. Di Giusto, C., Perez, J.A.: Disciplined structured communications with disciplined runtime adaptation. Sci. Comput. Program. 97(2), 235–265 (2015)

    Article  Google Scholar 

  95. Goldberg, A., Havelund, K.: Automated runtime verification with Eagle. In: Modelling, Simulation, Verification and Validation of Enterprise Information Systems, Proceedings of the 3rd International Workshop on Modelling, Simulation, Verification and Validation of Enterprise Information Systems, MSVVEIS 2005, In Conjunction with ICEIS 2005, Miami, FL, USA, May 2005

    Google Scholar 

  96. Haghighi, I., Jones, A., Kong, Z., Bartocci, E., Grosu, R., Belta, C.:. SpaTeL: a novel spatial-temporal logic and its applications to networked systems. In: Proceedings of HSCC 2015: The 18th International Conference on Hybrid Systems: Computation and Control, pp. 189–198. IEEE (2015)

    Google Scholar 

  97. Hallé, S., Villemaire, R.: Runtime monitoring of message-based workflows with data. In: ECOC 2008, pp. 63–72. IEEE Computer Society (2008)

    Google Scholar 

  98. Hauswirth, M., Chilimbi, T.M.: Low-overhead memory leak detection using adaptive statistical profiling. In: Proceedings of ASPLOS: The 11th International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 156–164. ACM (2004)

    Google Scholar 

  99. Havelund, K.: Rule-based runtime verification revisited. STTT 17(2), 143–170 (2015)

    Article  Google Scholar 

  100. Havelund, K., Goldberg, A.: Verify your runs. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 374–383. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-69149-5_40

    Chapter  Google Scholar 

  101. Havelund, K., Reger, G.: Runtime verification logics a language design perspective. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools: Essays Dedicated to Kim Guldstrand Larsen on the Occasion of His 60th Birthday. LNCS, vol. 10460, pp. 310–338. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63121-9_16

    Chapter  Google Scholar 

  102. Havelund, K., Reger, G., Zalinescu, E., Thoma, D.: Monitoring events that carry data. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 61–102. Springer, Cham (2018)

    Chapter  Google Scholar 

  103. Huang, X., Seyster, J., Callanan, S., Dixit, K., Grosu, R., Smolka, S.A., Stoller, S.D., Zadok, E.: Software monitoring with controllable overhead. STTT 14(3), 327–347 (2012)

    Article  Google Scholar 

  104. Jaksic, S., Bartocci, E., Grosu, R., Kloibhofer, R., Nguyen, T., Ničković, D.: From signal temporal logic to FPGA monitors. In: Proceedings of MEMOCODE 2015: The 13th ACM/IEEE International Conference on Formal Methods and Models for Codesign, pp. 218–227. IEEE (2015)

    Google Scholar 

  105. Jakšić, S., Bartocci, E., Grosu, R., Ničković, D.: Quantitative monitoring of STL with edit distance. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 201–218. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_13

    Chapter  Google Scholar 

  106. Kalajdzic, K., Bartocci, E., Smolka, S.A., Stoller, S.D., Grosu, R.: Runtime verification with particle filtering. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 149–166. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_9

    Chapter  Google Scholar 

  107. Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of AspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–354. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45337-7_18

    Chapter  Google Scholar 

  108. Kim, M., Kannan, S., Lee, I., Sokolsky, O., Viswanathan, M.: Computational analysis of run-time monitoring - fundamentals of Java-MaC. Electr. Notes Theor. Comput. Sci. 70(4), 80–94 (2002)

    Article  Google Scholar 

  109. Laurent, J., Goodloe, A., Pike, L.: Assuring the guardians. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 87–101. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_6

    Chapter  Google Scholar 

  110. Laurenzano, M., Tikir, M.M., Carrington, L., Snavely, A.: PEBIL: efficient static binary instrumentation for Linux. In: IEEE International Symposium on Performance Analysis of Systems and Software, ISPASS 2010, 28–30 March 2010, White Plains, NY, USA, pp. 175–183. IEEE Computer Society (2010)

    Google Scholar 

  111. Leucker, M., Sánchez, C.: Regular linear temporal logic. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 291–305. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_20

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  113. Libkin, L., Vrgoč, D.: Regular expressions for data words. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 274–288. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28717-6_22

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  115. Lourenço, J., Fiedor, J., Krena, B., Vojnar, T.: Discovering concurrency errors. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 34–60. Springer, Cham (2018)

    Chapter  Google Scholar 

  116. Luk, C.-K., Cohn, R.S., Muth, R., Patil, H., Klauser, A., Lowney, P.G., Wallace, S., Reddi, V.J., Hazelwood, K.M.: Pin: building customized program analysis tools with dynamic instrumentation. In: Proceedings of the ACM SIGPLAN 2005: The Conference on Programming Language Design and Implementation, pp. 190–200. ACM (2005)

    Google Scholar 

  117. Luo, Q., Roşu, G.: EnforceMOP: a runtime property enforcement system for multithreaded programs. In: ISSTA. ACM, New York (2013)

    Google Scholar 

  118. Majma, N., Babamir, S.M., Monadjemi, A.: Runtime verification of pacemaker using fuzzy logic and colored petri-nets. In: 2015 4th Iranian Joint Congress on Fuzzy and Intelligent Systems (CFIS), pp. 1–5, September 2015

    Google Scholar 

  119. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_12

    Chapter  Google Scholar 

  120. Meredith, P., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Transf. 14(3), 249–289 (2012). https://doi.org/10.1007/s10009-011-0198-6

    Article  Google Scholar 

  121. Nanda, S., Li, W., Lam, L.-C., Chiueh, T.: BIRD: binary interpretation using runtime disassembly. In: Proceedings of CGO 2006: The Fourth IEEE/ACM International Symposium on Code Generation and Optimization, pp. 358–370. IEEE Computer Society (2006)

    Google Scholar 

  122. Nazarpour, H., Falcone, Y., Bensalem, S., Bozga, M.: Concurrency-preserving and sound monitoring of multi-threaded component-based systems: theory, algorithms, implementation, and evaluation. Formal Asp. Comput. 29(6), 951–986 (2017)

    Article  MathSciNet  MATH  Google Scholar 

  123. Nenzi, L., Bortolussi, L., Ciancia, V., Loreti, M., Massink, M.: Qualitative and quantitative monitoring of spatio-temporal properties. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 21–37. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_2

    Chapter  Google Scholar 

  124. Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pp. 89–100. ACM (2007)

    Google Scholar 

  125. Nguyen, T., Bartocci, E., Ničković, D., Grosu, R., Jaksic, S., Selyunin, K.: The HARMONIA project: hardware monitoring for automotive systems-of-systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 371–379. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_28

    Chapter  Google Scholar 

  126. Pintér, G., Majzik, I.: Runtime verification of statechart implementations. In: de Lemos, R., Gacek, C., Romanovsky, A. (eds.) WADS -2004. LNCS, vol. 3549, pp. 148–172. Springer, Heidelberg (2005). https://doi.org/10.1007/11556169_7

    Chapter  Google Scholar 

  127. Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46–57. IEEE Computer Society, Washington, DC (1977)

    Google Scholar 

  128. Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573–586. Springer, Heidelberg (2006). https://doi.org/10.1007/11813040_38

    Chapter  Google Scholar 

  129. Reger, G., Havelund, K.: What is a trace? A runtime verification perspective. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 339–355. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47169-3_25

    Chapter  Google Scholar 

  130. 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, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_14

    Chapter  Google Scholar 

  131. Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Eng. 12(2), 151–197 (2005)

    Article  Google Scholar 

  132. Roşu, G., Bensalem, S.: Allen linear (interval) temporal logic – translation to LTL and monitor synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 263–277. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_25

    Chapter  Google Scholar 

  133. Saidi, S., Falcone, Y.: Dynamic detection and mitigation of DMA races in MPSoCs. In: 2015 Euromicro Conference on Digital System Design, DSD 2015, Madeira, Portugal, 26–28 August 2015, pp. 267–270. IEEE Computer Society (2015)

    Google Scholar 

  134. Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)

    Article  Google Scholar 

  135. Selyunin, K., Jaksic, S., Nguyen, T., Reidl, C., Hafner, U., Bartocci, E., Nickovic, D., Grosu, R.: Runtime monitoring with recovery of the SENT communication protocol. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 336–355. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_17

    Chapter  Google Scholar 

  136. Selyunin, K., Nguyen, T., Bartocci, E., Grosu, R.: Applying runtime monitoring for automotive electronic development. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 462–469. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_30

    Chapter  Google Scholar 

  137. Selyunin, K., Nguyen, T., Bartocci, E., Ničković, D., Grosu, R.: Monitoring of MTL specifications with IBM’s spiking-neuron model. In: Proceedings of DATE 2016: The 2016 Design, Automation & Test in Europe Conference, pp. 924–929. IEEE (2016)

    Google Scholar 

  138. Sen, K., Vardhan, A., Agha, G., Roşu, G.: Efficient decentralized monitoring of safety in distributed systems. In: ICSE, pp. 418–427 (2004)

    Google Scholar 

  139. Seyster, J., Dixit, K., Huang, X., Grosu, R., Havelund, K., Smolka, S.A., Stoller, S.D., Zadok, E.: Interaspect: aspect-oriented instrumentation with GCC. Form. Methods Syst. Des. 41(3), 295–320 (2012)

    Article  MATH  Google Scholar 

  140. Sokolsky, O., Havelund, K., Lee, I.: Introduction to the special section on runtime verification. STTT 14(3), 243–247 (2012)

    Article  Google Scholar 

  141. Spinczyk, O., Lohmann, D.: The design and implementation of AspectC++. Know.-Based Syst. 20(7), 636–651 (2007)

    Article  Google Scholar 

  142. Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193–207. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_15

    Chapter  Google Scholar 

  143. Stollon, N.: On-Chip Instrumentation. Springer, New York (2011). https://doi.org/10.1007/978-1-4419-7563-8

    Book  MATH  Google Scholar 

  144. Stolz, V.: Temporal assertions with parametrized propositions. J. Log. Comput. 20(3), 743–757 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  145. Thati, P., Roşu, G.: Monitoring algorithms for metric temporal logic specifications. Electron. Notes Theor. Comput. Sci. 113, 145–162 (2005)

    Article  Google Scholar 

  146. Winslett, M.: Bruce lindsay speaks out: on System R, benchmarking, life as an IBM fellow, the power of DBAs in the old days, why performance still matters, heisenbugs, why he still writes code, singing pigs, and more. SIGMOD Rec. 34(2), 71–79 (2005)

    Article  Google Scholar 

  147. Zhou, S., Zedan, H., Cau, A.: Run-time analysis of time-critical systems. J. Syst. Archit. 51(5), 331–345 (2005)

    Article  Google Scholar 

Download references

Acknowledgment

All the authors acknowledge the support of the ICT COST Action IC1402 Runtime Verification beyond Monitoring (ARVI). Ezio Bartocci acknowledges the Austrian National Research Network (nr. S 11405-N23) SHiNE funded by the Austrian Science Fund (FWF).

Author information

Authors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Univ. Grenoble Alpes, Inria, CNRS, Grenoble INP, Laboratoire d’Informatique de Grenoble, 38000, Grenoble, France

    Yliès Falcone

  3. University of Malta, Msida, MSD 2080, Malta

    Adrian Francalanza

  4. University of Manchester, Manchester, UK

    Giles Reger

Authors
  1. Ezio Bartocci
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yliès Falcone
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adrian Francalanza
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Giles Reger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ezio Bartocci .

Editor information

Editors and Affiliations

  1. TU Wien, Vienna, Austria

    Ezio Bartocci

  2. Université Grenoble Alpes, Inria, Laboratoire d’Informatique de Grenoble, Grenoble, France

    Yliès Falcone

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bartocci, E., Falcone, Y., Francalanza, A., Reger, G. (2018). Introduction to Runtime Verification. In: Bartocci, E., Falcone, Y. (eds) Lectures on Runtime Verification. Lecture Notes in Computer Science(), vol 10457. Springer, Cham. https://doi.org/10.1007/978-3-319-75632-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-75632-5_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-75631-8

  • Online ISBN: 978-3-319-75632-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation