Top

Published in:

2018 | OriginalPaper | Chapter

Monitoring Events that Carry Data

Authors : Klaus Havelund, Giles Reger, Daniel Thoma, Eugen Zălinescu

Published in: Lectures on Runtime Verification

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Very early runtime verification systems focused on monitoring what we can refer to as propositional events: just names of events. For this, finite state machines, standard regular expressions, or propositional temporal logics were sufficient formalisms for expressing properties. However, in practice there is a need for monitoring events that in addition carry data arguments. This adds complexity to both the property specification languages, and monitoring algorithms, which is reflected in the many alternative such approaches suggested in the literature. This chapter presents five different formalisms and monitoring approaches that support specifications with data, in order to illustrate the challenges and various solutions.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Discovering Concurrency Errors

next chapter Runtime Failure Prevention and Reaction

Since we restrict ourselves to the past-only fragment of FOTL, the outermost temporal operator \({\square }\) (“always”) is not part of our definition of the logic given in Sect. 3.2. However, we include it in the formalisation to emphasise that the property must be fulfilled at all time points.

When considering specifications with a future dimension, see [17], we require that future operators are bounded: they only look boundedly far into the future; this corresponds to hard-time specifications, and can be specified with metric temporal constraints; that is in Metric FOTL [53]. Note that the approach thus handles a safety fragment of (Metric) FOTL. Then, to handle a finite trace, since it is assumed that time is observed by the monitoring algorithm only through event timestamps, a new dummy event with a sufficiently large timestamp is added at the end of the trace, and the algorithm is stopped after observing this last event.

Note that here we treat the operator \(\wedge \) as a primitive.

The notion of domain independence [4, 17] intuitively requires that the satisfying valuations of a formula are independent of the domain of quantification. This semantic notion is laxer than the monitorability requirement, and also guarantees finiteness of \([\![\psi ]\!]^{i}\), but is, however, undecidable.

A complete lattice is a partial order \((M, \sqsubseteq )\) where every subset \(N \subseteq M\) has a least upper bound \(\sqcup N\) and a greatest lower bound \(\sqcap N\).

A one-to-one mapping from F to \( AP \) can be defined, but we refrain to do so, for simplicity.

These relate directly to the notion of event, as in Sect. 3 (see Remark 1). E.g., the event \(\mathsf {create}(\mathsf {m}_1,\mathsf {c}_1)\) would be represented as the structure interpreting \(\mathsf {create}\) as the set \(\{(\mathsf {m}_1,\mathsf {c}_1) \}\).

In the more general framework constraints must contain interpreted predicates only.

The syntax has been modified slightly from Scala to a more mathematical notation.

Providing a full definition of LogFire would be too space consuming for this presentation.

A Scala version of this semantics has been developed.

An implementation can be found at https://www.react.uni-saarland.de/tools/lola/.

We abuse notation and apply them on unnamed relations, as their attributes are as expected, e.g. \(\langle m,c \rangle \) for \(\mathsf {createdC}\), and \(\langle c,i,m \rangle \) for \(\mathsf {createdI}\) and \(\mathsf {updated}\).

In examples we do not make a distinction between stream variables and their denoted streams, that is, we identify x and \(\theta (x)\).

This assumption is not satisfied for our formalisations of the UnsafeMapIterator property.

Assuming a guard and assignment language such that checking QEA emptiness is decidable.

Bindings whose values are explicitly connected by events in the trace.

Clips website. http://clipsrules.sourceforge.net

Drools website. http://www.jboss.org/drools

Rooscaloo website. https://github.com/daveray/rooscaloo

Abiteboul, S., Hull, R., Vianu, V.: Foundations of Databases: The Logical Level. Addison Wesley, Boston (1994)

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)CrossRefMATH

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 CrossRef

Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–204 (1994)MathSciNetCrossRefMATH

Ballarin, C.: Two generalisations of Roşu and Chen’s trace slicing algorithm A. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 15–30. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_3

Barringer, H., Rydeheard, D., Havelund, K.: Rule systems for run-time monitoring: from Eagle to Ruler. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 111–125. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77395-5_10 CrossRef

10.

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 CrossRef

11.

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 CrossRef

12.

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 CrossRef

13.

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)MathSciNetCrossRefMATH

14.

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. Trans. 1–40 (2017)

15.

Basin, D., Harvan, M., Klaedtke, F., Zălinescu, E.: MONPOLY: monitoring usage-control policies. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 360–364. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_27 CrossRef

16.

Basin, D.A., Klaedtke, F., Marinovic, S., Zălinescu, E.: Monitoring of temporal first-order properties with aggregations. Form. Method. Syst. Des. 46(3), 262–285 (2015)CrossRefMATH

17.

Basin, D.A., Klaedtke, F., Müller, S., Zălinescu, E.: Monitoring metric first-order temporal properties. J. ACM 62(2), 15 (2015)MathSciNetCrossRefMATH

18.

Bauer, A., Goré, R., Tiu, A.: A first-order policy language for history-based transaction monitoring. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 96–111. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03466-4_6 CrossRef

19.

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

20.

Bauer, A., Leucker, M., Schallhart, C.: Monitoring of real-time properties. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 260–272. Springer, Heidelberg (2006). https://doi.org/10.1007/11944836_25 CrossRef

21.

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 CrossRef

22.

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

23.

Berry, G.: The foundations of Esterel. In: Plotkin, G., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 425–454. MIT Press, Cambridge (2000)

24.

Bozzelli, L., Sánchez, C.: Foundations of Boolean stream runtime verification. Theoret. Comput. Sci. 631, 118–138 (2016)MathSciNetCrossRefMATH

25.

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 CrossRef

26.

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

27.

Chowdhury, O., Jia, L., Garg, D., Datta, A.: Temporal mode-checking for runtime monitoring of privacy policies. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 131–149. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_9

28.

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

29.

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: Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, pp. 166–174. IEEE Computer Society (2005)

30.

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). https://doi.org/10.1007/978-3-662-49674-9_54 CrossRef

31.

Decker, N., Leucker, M., Thoma, D.: Impartiality and anticipation for monitoring of visibly context-free properties. In: Legay, A., Bensalem, S. (eds.) RV 2013. LNCS, vol. 8174, pp. 183–200. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40787-1_11 CrossRef

32.

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

33.

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). https://doi.org/10.1007/978-3-642-54862-8_23 CrossRef

34.

Decker, N., Leucker, M., Thoma, D.: Monitoring modulo theories. Int. J. Softw. Tools Technol. Trans. 18(2), 205–225 (2016)CrossRef

35.

Dong, W., Leucker, M., Schallhart, C.: Impartial anticipation in runtime-verification. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 386–396. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-88387-6_33 CrossRef

36.

Doorenbos, R.B.: Production matching for large learning systems. Ph.D. thesis, Carnegie Mellon University, Pittsburgh, PA (1995)

37.

Eisner, C., Fisman, D., Havlicek, J., Lustig, Y., McIsaac, A., Van Campenhout, D.: Reasoning with temporal logic on truncated paths. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 27–39. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_3 CrossRef

38.

Falcone, Y., Ničković, 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, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_27 CrossRef

39.

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 CrossRef

40.

Forgy, C.: Rete: a fast algorithm for the many pattern/many object pattern match problem. Artif. Intell. 19, 17–37 (1982)CrossRef

41.

Fusco, M.: Hammurabi - a Scala rule engine. In: Scala Days 2011, Stanford University, California (2011)

42.

Garcia-Molina, H., Ullman, J.D., Widom, J.: Database Systems: The Complete Book. Pearson Education, Upper Saddle River (2009)

43.

Goubault-Larrecq, J., Olivain, J.: A smell of ORCHIDS. In: Leucker, M. (ed.) RV 2008. LNCS, vol. 5289, pp. 1–20. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89247-2_1 CrossRef

44.

Håkansson, J., Jonsson, B., Lundqvist, O.: Generating online test oracles from temporal logic specifications. Int. J. Softw. Tools Technol. Trans. 4(4), 456–471 (2003)CrossRef

45.

Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991)CrossRef

46.

Hallé, S., Villemaire, R.: Runtime enforcement of web service message contracts with data. IEEE Trans. Servic. Comput. 5(2), 192–206 (2012)CrossRef

47.

Havelund, K.: Rule-based runtime verification revisited. Int. J. Softw. Tools Technol. Trans. 17(2), 143–170 (2015)CrossRef

48.

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 CrossRef

49.

Herzeel, C., Gybels, K., Costanza, P.: Escaping with future variables in HALO. In: Sokolsky, O., Taşıran, S. (eds.) RV 2007. LNCS, vol. 4839, pp. 51–62. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-77395-5_5 CrossRef

50.

Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order temporal logics. Ann. Pure Appl. Log. 106(1–3), 85–134 (2000)MathSciNetCrossRefMATH

51.

Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)

52.

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. (2007)

53.

Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)CrossRef

54.

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 CrossRef

55.

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

56.

Meredith, P.O., Jin, D., Griffith, D., Chen, F., Roşu, G.: An overview of the MOP runtime verification framework. Int. J. Softw. Tools Technol. Trans. 14(3), 249–289 (2012)CrossRef

57.

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). https://doi.org/10.1007/978-3-642-29860-8_31 CrossRef

58.

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

59.

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). https://doi.org/10.1007/978-3-662-46681-0_55

60.

Reger, G., Hallé, S., Falcone, Y.: Third international competition on runtime verification. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 21–37. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_3 CrossRef

61.

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 CrossRef

62.

Roşu, G., Chen, F.: Semantics and algorithms for parametric monitoring. Log. Methods Comput. Sci. 8(1), 1–47 (2012)MathSciNetMATH

63.

Stolz, V.: Temporal assertions with parameterized propositions. J. Logic Comput. 20(3), 743–757 (2010)MathSciNetCrossRefMATH

64.

Stolz, V., Bodden, E.: Temporal assertions using AspectJ. In: Proceeding of the 5th International Workshop on Runtime Verification (RV 2005). ENTCS, vol. 144(4), pp. 109–124. Elsevier (2006)

Title: Monitoring Events that Carry Data
Authors: Klaus Havelund
Giles Reger
Daniel Thoma
Eugen Zălinescu
Publisher: Springer International Publishing
Book: Lectures on Runtime Verification
Print ISBN: 978-3-319-75631-8

Electronic ISBN: 978-3-319-75632-5

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-75632-5_3

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner