Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Formal Methods in System Design
Published in: Formal Methods in System Design 1/2017

24-03-2017

Monitorability for the Hennessy–Milner logic with recursion

Authors: Adrian Francalanza, Luca Aceto, Anna Ingolfsdottir

Published in: Formal Methods in System Design | Issue 1/2017

Log in

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

search-config
loading …

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.
previous article Collision avoidance for mobile robots with limited sensing and limited information about moving obstacles
next article Formal analysis and offline monitoring of electronic exams

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 "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

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
Footnotes
1
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.
 
2
A transition sequence is maximal if it is either infinite or affords no more actions.
 
Literature
1.
Abrial J R (2010) Modeling in event-B: system and software engineering. Cambridge University Press, CambridgeCrossRefMATH
2.
Aceto L, Ingólfsdóttir A (1999) Testing Hennessy–Milner logic with recursion. In: FoSSaCS’99. Springer, Berlin, pp 41–55
3.
Aceto L, Ingólfsdóttir A, Larsen KG, Srba J (2007) Reactive systems: modelling, specification and verification. Cambridge University Press, New YorkCrossRefMATH
4.
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
5.
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
6.
Attard DP, Francalanza A (2016) A monitoring tool for a branching-time logic. In: RV, vol 10012 of LNCS. Springer, Berlin, pp 473–481
7.
Baier C, Katoen JP (2008) Principles of model checking. MIT Press, New YorkMATH
8.
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
9.
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.
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.
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.
30.
31.
Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebraic Program 78(5):293–303CrossRefMATH
32.
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.
38.
Vella A, Francalanza A (2016) Preliminary results towards contract monitorability. In: PrePost, vol 208 of EPTCS, pp 54–63
Metadata
Title
Monitorability for the Hennessy–Milner logic with recursion
Authors
Adrian Francalanza
Luca Aceto
Anna Ingolfsdottir
Publication date
24-03-2017
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 1/2017
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0273-z

Other articles of this Issue 1/2017

Formal Methods in System Design 1/2017 Go to the issue

OriginalPaper

Formal analysis and offline monitoring of electronic exams

OriginalPaper

Predictive runtime enforcement

OriginalPaper

Introduction to the special issue on runtime verification

OriginalPaper

R2U2: monitoring and diagnosis of security threats for unmanned aerial systems

OriginalPaper

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

OriginalPaper

Robust online monitoring of signal temporal logic

Premium Partner

    Image Credits