nach oben

Formal Methods in System Design

Erschienen in:

24.03.2017

Monitorability for the Hennessy–Milner logic with recursion

verfasst von: Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir

Erschienen in: Formal Methods in System Design | Ausgabe 1/2017

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We study \(\mu \) HML, a branching-time logic with least and greatest fixpoints, from a runtime verification perspective. The logic may be used to specify properties of programs whose behaviour may be expressed as a labelled transition system. We establish which subset of this logic can be monitored for at runtime by merely observing the runtime execution of a program. A monitor-synthesis algorithm is defined for this subset, where it is shown that the resulting synthesised monitors correctly perform the required analysis from the observed behaviour. We also prove completeness results wrt. this logical subset that show that, up to logical equivalence, no other properties apart from those identified can be monitored for and verified at runtime.

Vorheriger Artikel Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles

Nächster Artikel Formal analysis and offline monitoring of electronic exams

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

These are normally expressed as structural equivalence rules such as \(p\!\parallel \!\textsf {nil} \equiv p\) and \(p\!\parallel \!q \equiv q\!\parallel \!p\) in standard CCS. We elide them here to alleviate our exposition.

A transition sequence is maximal if it is either infinite or affords no more actions.

Abrial J R (2010) Modeling in event-B: system and software engineering. Cambridge University Press, CambridgeCrossRefMATH

Aceto L, Ingólfsdóttir A (1999) Testing Hennessy–Milner logic with recursion. In: FoSSaCS’99. Springer, Berlin, pp 41–55

Aceto L, Ingólfsdóttir A, Larsen KG, Srba J (2007) Reactive systems: modelling, specification and verification. Cambridge University Press, New YorkCrossRefMATH

Ahrendt W, Chimento JM, Pace GJ, Schneider G (2015) A specification language for static and runtime verification of data and control properties. In: FM 2015, vol 9109. Springer, Berlin, pp 108–125

Andersen JR, Andersen N, Enevoldsen S, Hansen MM, Larsen KG, Olesen SR, Srba J, Wortmann J (2015) CAAL: concurrency workbench, Aalborg Edition. In: ICTAC. Springer, Berlin, pp 573–582

Attard DP, Francalanza A (2016) A monitoring tool for a branching-time logic. In: RV, vol 10012 of LNCS. Springer, Berlin, pp 473–481

Baier C, Katoen JP (2008) Principles of model checking. MIT Press, New YorkMATH

Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard DE (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: FM, vol 7436 of LNCS. Springer, Berlin, pp 68–84

Barringer H, Goldberg A, Havelund K, Sen K (2004) Rule-based runtime verification. In: VMCAI, vol 2937 of LNCS, Springer, Berlin, pp 44–57

10.

Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: RV, vol 4839 of LNCS. Springer, Berlin, pp 126–138

11.

Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for runtime verification. Log Comput 20(3):651–674MathSciNetCrossRefMATH

12.

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

13.

Cassar I, Francalanza A (2014) On synchronous and asynchronous monitor instrumentation for actor systems. FOCLASA 175:54–68MathSciNet

14.

Cassar I, Francalanza A (2015) Runtime adaptation for actor systems. In: Runtime verification (RV), vol 9333 of LNCS. Springer, Berlin, pp 38–54

15.

Cassar I, Francalanza A (2016) On implementing a monitor-oriented programming framework for actor systems. In: iFM, vol 9681 of LNCS, pp 176–192

16.

Cerone A, Hennessy M (2010) Process behaviour: formulae versus tests. In: EXPRESS, vol 41 of EPTCS, pp 31–45

17.

Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: ALP LNCS. Springer, Berlin, pp 474–486

18.

Cini C, Francalanza A (2015) An LTL proof system for runtime verification. In: TACAS, vol 9035. Springer, Berlin, pp 581–595

19.

Clarke EM Jr, Grumberg O, Peled DA (1999) Model checking. MIT Press, Cambridge

20.

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

21.

Eisner C, Fisman D, Havlicek J, Lustig Y, McIsaac A, Campenhout DV (2003) Reasoning with temporal logic on truncated paths. In: CAV, vol 2725 of LNCS. Springer, Berlin, pp 27–39

22.

Falcone Y, Fernandez J-C, Mounier L (2012) What can you verify and enforce at runtime? Softw Tools Technol Transf 14(3):349–382CrossRef

23.

Francalanza A (2016) A theory of monitors (extended abstract). In: FoSSaCS, vol 9634 of LNCS. Springer, Berlin, pp 145–161

24.

Francalanza A, Aceto L, Ingólfsdóttir A (2015) On verifying Hennessy–Milner logic with recursion at runtime. In: RV, vol 9333 of LNCS, pp 71–86

25.

Francalanza A, Gauci A, Pace GJ (2013) Distributed system contract monitoring. J Log Algebr Program 82(5–7):186–215MathSciNetCrossRefMATH

26.

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

27.

Geilen M (2001) On the construction of monitors for temporal logic properties. In: RV, vol 55 of ENTCS, pp 181–199

28.

Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs

29.

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

30.

Larsen KG (1990) Proof systems for satisfiability in Hennessy–Milner logic with recursion. Theor Comput Sci 72(2):265–288MathSciNetCrossRefMATH

31.

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

32.

Manna Z, Pnueli A (1991) Completing the temporal picture. Theor Comput Sci 83(1):97–130CrossRefMATH

33.

Milner R (1982) A calculus of communicating systems. Springer, BerlinMATH

34.

Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: FM, vol 4085. Springer, Berlin, pp 573–586

35.

Sen K, Rosu G, Agha G (2003) Generating optimal linear temporal logic monitors by coinduction. In: ASIAN, vol 2896 of LNCS, Springer, Berlin, pp 260–275

36.

Shi J, Lahiri SK, Chandra R, Challen G. Wireless protocol validation under uncertainty. In: RV

37.

detectEr Project. http://www.cs.um.edu.mt/svrg/Tools/detectEr/

38.

Vella A, Francalanza A (2016) Preliminary results towards contract monitorability. In: PrePost, vol 208 of EPTCS, pp 54–63

Titel: Monitorability for the Hennessy–Milner logic with recursion
verfasst von: Adrian Francalanza
Luca Aceto
Anna Ingolfsdottir
Publikationsdatum: 24.03.2017
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 1/2017
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-017-0273-z

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2017

Formal analysis and offline monitoring of electronic exams

Predictive runtime enforcement

Robust online monitoring of signal temporal logic

Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles

Verifying data- and control-oriented properties combining static and runtime verification: theory and tools

Introduction to the special issue on runtime verification

Premium Partner