Skip to main content

2016 | OriginalPaper | Buchkapitel

A Theory of Monitors

(Extended Abstract)

verfasst von : Adrian Francalanza

Erschienen in: Foundations of Software Science and Computation Structures

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We develop a behavioural theory for monitors — software entities that passively analyse the runtime behaviour of systems so as to infer properties about them. First, we extend the monitor language and instrumentation relation of [17] to handle piCalculus process monitoring. We then identify contextual behavioural preorders that allow us to relate monitors according to criteria defined over monitored executions of piCalculus processes. Subsequently, we develop alternative monitor preorders that are more tractable, and prove full-abstraction for the latter alternative preorders with respect to the contextual preorders.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

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!

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!

Fußnoten
1
The rules in Fig. 1 still check explicitly for this; see rules pRes, pCls and pOpn.
 
Literatur
1.
Zurück zum Zitat Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: 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)CrossRef Barringer, H., Falcone, Y., Havelund, K., Reger, G., Rydeheard, D.E.: 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)CrossRef
2.
Zurück zum Zitat Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 20(4), 14 (2011)CrossRef Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. TOSEM 20(4), 14 (2011)CrossRef
4.
Zurück zum Zitat Bielova, N., Massacci, F.: Do you really mean what you actually enforced? Edited automata revisited. Int. J. Inf. Secur. 10(4), 239–254 (2011)CrossRef Bielova, N., Massacci, F.: Do you really mean what you actually enforced? Edited automata revisited. Int. J. Inf. Secur. 10(4), 239–254 (2011)CrossRef
5.
Zurück zum Zitat Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013)CrossRef Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013)CrossRef
6.
Zurück zum Zitat Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor systems. FOCLASA 175, 54–68 (2014) Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor systems. FOCLASA 175, 54–68 (2014)
7.
Zurück zum Zitat Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_7 CrossRef Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-23820-3_​7 CrossRef
8.
Zurück zum Zitat Cesarini, F., Thompson, S.: Erlang Programming. O’Reilly, Sebastopol (2009)MATH Cesarini, F., Thompson, S.: Erlang Programming. O’Reilly, Sebastopol (2009)MATH
9.
Zurück zum Zitat Chen, F., Roşu, G.: MOP: An efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588. ACM, (2007) Chen, F., Roşu, G.: MOP: An efficient and generic runtime verification framework. In: OOPSLA, pp. 569–588. ACM, (2007)
10.
Zurück zum Zitat 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) 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)
11.
Zurück zum Zitat Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Self-adaptive monitors for multiparty sessions. In: PDP, pp. 688–696. IEEE Computer Society (2014) Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Self-adaptive monitors for multiparty sessions. In: PDP, pp. 688–696. IEEE Computer Society (2014)
12.
Zurück zum Zitat 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, IEEE (2005) 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, IEEE (2005)
14.
Zurück zum Zitat Decker, N., Leucker, M., Thoma, D.: jUnit\(^\text{ 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)CrossRef Decker, N., Leucker, M., Thoma, D.: jUnit\(^\text{ 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)CrossRef
15.
Zurück zum Zitat Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRef Falcone, Y., Fernandez, J.-C., Mounier, L.: What can you verify and enforce at runtime? STTT 14(3), 349–382 (2012)CrossRef
17.
Zurück zum Zitat Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_7 CrossRef Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an autonomous research vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-23820-3_​7 CrossRef
18.
Zurück zum Zitat Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5–7), 186–215 (2013)MathSciNetMATH Francalanza, A., Gauci, A., Pace, G.J.: Distributed system contract monitoring. JLAP 82(5–7), 186–215 (2013)MathSciNetMATH
19.
Zurück zum Zitat Francalanza, A., Hennessy, M.: A theory for observational fault tolerance. JLAP 73(1–2), 22–50 (2007)MathSciNetMATH Francalanza, A., Hennessy, M.: A theory for observational fault tolerance. JLAP 73(1–2), 22–50 (2007)MathSciNetMATH
20.
Zurück zum Zitat Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. FMSD 46(3), 226–261 (2015)MATH Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. FMSD 46(3), 226–261 (2015)MATH
21.
Zurück zum Zitat Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 1–61 (2009)CrossRefMATH Castagna, G., Gesbert, N., Padovani, L.: A theory of contracts for web services. ACM Trans. Program. Lang. Syst. 31(5), 1–61 (2009)CrossRefMATH
22.
Zurück zum Zitat Giusto, C.D., Perez, J.A.: Disciplined structured communications with disciplined runtime adaptation. Sci. Comput. Program. 97(2), 235–265 (2015)CrossRef Giusto, C.D., Perez, J.A.: Disciplined structured communications with disciplined runtime adaptation. Sci. Comput. Program. 97(2), 235–265 (2015)CrossRef
23.
Zurück zum Zitat Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)MATH Hennessy, M.: Algebraic Theory of Processes. MIT Press, Cambridge (1988)MATH
24.
Zurück zum Zitat Hennessy, M.: A Distributed Pi-Calculus. Cambridge University Press, Cambridge (2007)CrossRefMATH Hennessy, M.: A Distributed Pi-Calculus. Cambridge University Press, Cambridge (2007)CrossRefMATH
25.
Zurück zum Zitat Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: A run-time assurance approach for Java programs. FMSD 24(2), 129–155 (2004)MATH Kim, M., Viswanathan, M., Kannan, S., Lee, I., Sokolsky, O.: Java-MaC: A run-time assurance approach for Java programs. FMSD 24(2), 129–155 (2004)MATH
26.
Zurück zum Zitat Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an Autonomous Research Vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_7 CrossRef Kane, A., Chowdhury, O., Datta, A., Koopman, P.: A case study on runtime monitoring of an Autonomous Research Vehicle (ARV) system. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 102–117. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-23820-3_​7 CrossRef
27.
Zurück zum Zitat Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293–303 (2009)MATH Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293–303 (2009)MATH
28.
Zurück zum Zitat 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)CrossRef 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)CrossRef
29.
Zurück zum Zitat Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)MATH Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)MATH
30.
Zurück zum Zitat Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Engg. 12(2), 151–197 (2005)CrossRef Roşu, G., Havelund, K.: Rewriting-based techniques for runtime verification. Autom. Softw. Engg. 12(2), 151–197 (2005)CrossRef
31.
Zurück zum Zitat Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH Sangiorgi, D., Walker, D.: PI-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)MATH
32.
Zurück zum Zitat Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)CrossRef Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)CrossRef
33.
Zurück zum Zitat Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: ICSE, pp. 418–427. IEEE (2004) Sen, K., Vardhan, A., Agha, G., Rosu, G.: Efficient decentralized monitoring of safety in distributed systems. In: ICSE, pp. 418–427. IEEE (2004)
34.
Zurück zum Zitat Verissimo, P., Rodrigues, L.: Distributed Systems for System Architects. Kluwer Academic Publishers, Norwell (2001)CrossRefMATH Verissimo, P., Rodrigues, L.: Distributed Systems for System Architects. Kluwer Academic Publishers, Norwell (2001)CrossRefMATH
Metadaten
Titel
A Theory of Monitors
verfasst von
Adrian Francalanza
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-49630-5_9

Premium Partner