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 3/2015

01-06-2015

Synthesising correct concurrent runtime monitors

Authors: Adrian Francalanza, Aldrin Seychell

Published in: Formal Methods in System Design | Issue 3/2015

Log in

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

search-config
loading …

Abstract

This paper studies the correctness of automated synthesis for concurrent monitors. We adapt a subset of the Hennessy–Milner logic with recursion (a reformulation of the modal \(\mu \)-calculus) to specify safety properties for Erlang programs. We also define an automated translation from formulas in this sub-logic to concurrent Erlang monitors that detect formula violations at runtime. Subsequently, we formalise a novel definition for monitor correctness that incorporates monitor behaviour when instrumented with the program being monitored. Finally, we devise a sound technique that allows us to prove monitor correctness in stages; this technique is used to prove the correctness of our automated monitor synthesis.
previous article Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
next article Monitoring of temporal first-order properties with aggregations

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
Appendix
Available only for authorised users
Footnotes
1
Due to \({\textsf {exit}}\) exceptions, variable bindings, \(x \,{\textsf {=}}\, e {\textsf {,}}\,d \) cannot be encoded as function applications, \( \uplambda x.d (e)\).
 
2
In our formalisation, expressions are not allowed to evaluate under a spawn context, \({\textsf {spw}}\, [-] \); this aspect differs from standard Erlang semantics but allows a lightweight description of function application spawning. An adjustment in line with the actual Erlang spawning would be straightforward.
 
3
Note that we do not show that sHML captures all the safety properties expressible in HMLwith recursion, and there are infact other formulas that specify safety properties such as \({\textsf {tt}}\).
 
4
Due to asynchronous communication, even scoped actors can produce visible actions by sending messages to environment actors.
 
5
One potential disadvantage of splitting formulas is that of increasing communication amongst monitors.
 
6
In guarded sHML formulas, variables appear only as a sub-formula of a necessity formula.
 
7
We elevate \({{\mathrm{tr}}}\) to basic action sequences \(s\) in pointwise fashion, \({{\mathrm{tr}}}(s)\), where \({{\mathrm{tr}}}(\epsilon )=\epsilon \).
 
Literature
1.
Aceto L, Ingólfsdóttir A (1999) Testing Hennessy–Milner logic with recursion. In: FoSSaCS’99. Springer, pp 41–55
2.
Aceto L, Ingólfsdóttir A, Larsen KG, Srba J (2007) Reactive systems: modelling. Specification and verification. Cambridge University Press, New YorkCrossRef
3.
Armstrong J (2007) Programming Erlang. The Pragmatic Bookshelf, Armstrong
4.
Bauer A, Falcone Y (2012) Decentralised LTL monitoring. In: Giannakopoulou D, Mry D (eds) FM. LNCS, vol 7436. Springer, pp 85–100
5.
Bauer A, Leucker M, Schallhar C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20:14:1–14:64CrossRef
6.
Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida N (2013) Monitoring networks through multiparty session types. In: FMOODS/FORTE 2013. LNCS, vol 7892. Springer, pp 50–65.
7.
Cao T-D, Phan-Quang T-T, Felix P, Castanet R (2010) Automated runtime verification for web services. In: ICWS. IEEE, pp 76–82
8.
Carlsson R (2001) An introduction to Core Erlang. In: PLI’01 (Erlang Workshop)
9.
Cassar I, Francalanza A (2014) On synchronous and asynchronous monitor instrumentation for actor-based systems. In: FOCLASA, EPTCS (to appear)
10.
Cerone A, Hennessy M (2010) Process behaviour: formulae vs. tests. In: EXPRESS’10, vol 41 EPTCS, pp 31–45
11.
Cesarini F, Thompson S (2009) Erlang programming. O’Reilly, SebastopolMATH
12.
Chang E, Manna Z, Pnueli A (1992) Characterization of temporal property classes. In: ALP. LNCS, vol 623. Springer-Verlag, pp 474–486
13.
Clarke E Jr, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
14.
Colombo C, Francalanza A, Gatt R (2011) Elarva: a monitoring tool for Erlang. In: RV. LNCS, vol 7186. Springer, pp 370–374
15.
Colombo C, Francalanza A, Grima I (2012) Simplifying contract-violating traces. In: FLACOS, EPTCS, vol 94, pp 11–20
16.
Colombo C, Francalanza A, Mizzi R, Pace GJ (2012) polylarva: runtime verification with configurable resource-aware monitoring boundaries. In: SEFM, pp 218–232
17.
D’Angelo B, Sankaranarayanan S, Sánchez C, Robinson W, Finkbeiner B, Sipma HB, Mehrotra S, Manna Z. (2005) Lola: runtime monitoring of synchronous systems. In: TIME, IEEE
18.
Falcone Y, Jaber M, Nguyen T-H, Bozga M, Bensalem S. (2011) Runtime verification of component-based systems. In: SEFM. LNCS, vol 7041. Springer, pp 204–220
19.
20.
Francalanza A, Gauci A, Pace GJ (2013) Distributed System contract monitoring. JLAP 82(5–7):186–215MATHMathSciNet
21.
22.
Fredlund L-Å (2001) A framework for reasoning about Erlang code. PhD thesis, Royal Institute of Technology, Stockholm, Sweden
23.
Geilen M (2001) On the construction of monitors for temporal logic properties. ENTCS 55(2):181–199
24.
Hennessy M (2008) A distributed picalculus. Cambridge University Proess, Cambridge
25.
Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137–161
26.
Hewitt C, Bishop P, Steiger R (1973) A universal modular actor formalism for artificial intelligence. In: IJCAI, Morgan Kaufmann, pp 235–245
27.
28.
Manna Z, Pnueli A (1990) A hierarchy of temporal properties (invited paper, 1989). In: PODC, ACM, pp 377–410
29.
Meredith PO, Jin D, Griffith D, Chen F, Rosu G (2012) An overview of the MOP runtime verification framework. STTT 14(3):249–289CrossRef
30.
Milner R (1989) Communication and concurrency. Prentice-Hall Inc, Upper Saddle RiverMATH
31.
32.
Nicola RD, Hennessy MCB (1984) Testing equivalences for processes, TCS, pp 83–133
33.
34.
Sen K, Rosu G, Agha G (2004) Generating optimal linear temporal logic monitors by coinduction. In: ASIAN. LNCS, vol 2896. Springer-Verlag, pp 260–275
35.
Sen K, Vardhan A, Agha G, Roşu G (2004) Efficient decentralized monitoring of safety in distributed systems. ICSE, pp 418–427
36.
Svensson H, Fredlund L-Å, Benac Earle C (2010) A unified semantics for future erlang. In: Erlang Workshop, ACM, pp 23–32
Metadata
Title
Synthesising correct concurrent runtime monitors
Authors
Adrian Francalanza
Aldrin Seychell
Publication date
01-06-2015
Publisher
Springer US
Published in
Formal Methods in System Design / Issue 3/2015
Print ISSN: 0925-9856
Electronic ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-014-0217-9

Other articles of this Issue 3/2015

Formal Methods in System Design 3/2015 Go to the issue

OriginalPaper

The ins and outs of first-order runtime verification

OriginalPaper

Monitoring of temporal first-order properties with aggregations

OriginalPaper

Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python

OriginalPaper

Runtime verification with minimal intrusion through parallelism

Premium Partner

    Image Credits