Skip to main content

2016 | OriginalPaper | Buchkapitel

A Monitoring Tool for a Branching-Time Logic

verfasst von : Duncan Paul Attard, Adrian Francalanza

Erschienen in: Runtime Verification

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

We present the implementation of an experimental tool that automatically synthesises monitors from specifications written in mHML, a monitorable subset of the branching-time logic \(\mu \)HML. The synthesis algorithm is compositional wrt the structure of the formula and follows closely a synthesis procedure that has been shown to be correct. We discuss how this compositionality facilitates a translation into concurrent Erlang monitors, where each individual (sub)monitor is an actor that autonomously analyses individual parts of the source specification formula while still guaranteeing the correctness of the overall monitoring process.

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!

Literatur
1.
Zurück zum Zitat Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor-based systems. In: FOCLASA, pp. 54–68 (2014) Cassar, I., Francalanza, A.: On synchronous and asynchronous monitor instrumentation for actor-based systems. In: FOCLASA, pp. 54–68 (2014)
2.
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
3.
Zurück zum Zitat Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying Hennessy-Milner logic with recursion at runtime. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 71–86. Springer, Heidelberg (2015). doi:10.1007/978-3-319-23820-3_5 CrossRef Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying Hennessy-Milner logic with recursion at runtime. In: Bartocci, E., et al. (eds.) RV 2015. LNCS, vol. 9333, pp. 71–86. Springer, Heidelberg (2015). doi:10.​1007/​978-3-319-23820-3_​5 CrossRef
4.
Zurück zum Zitat Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Met. Syst. Des. 46(3), 226–261 (2015)CrossRefMATH Francalanza, A., Seychell, A.: Synthesising correct concurrent runtime monitors. Formal Met. Syst. Des. 46(3), 226–261 (2015)CrossRefMATH
6.
Zurück zum Zitat Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97–130 (1991)CrossRefMATH Manna, Z., Pnueli, A.: Completing the temporal picture. Theor. Comput. Sci. 83(1), 97–130 (1991)CrossRefMATH
Metadaten
Titel
A Monitoring Tool for a Branching-Time Logic
verfasst von
Duncan Paul Attard
Adrian Francalanza
Copyright-Jahr
2016
DOI
https://doi.org/10.1007/978-3-319-46982-9_31

Premium Partner