nach oben

Formal Methods in System Design

Erschienen in:

01.06.2015

Synthesising correct concurrent runtime monitors

verfasst von: Adrian Francalanza, Aldrin Seychell

Erschienen in: Formal Methods in System Design | Ausgabe 3/2015

Einloggen

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

search-config

KI-gestützte Suche

Aus

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.

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

Nächster Artikel Monitoring of temporal first-order properties with aggregations

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

Nur mit Berechtigung zugänglich

Due to \({\textsf {exit}}\) exceptions, variable bindings, \(x \,{\textsf {=}}\, e {\textsf {,}}\,d \) cannot be encoded as function applications, \( \uplambda x.d (e)\).

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.

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}}\).

Due to asynchronous communication, even scoped actors can produce visible actions by sending messages to environment actors.

One potential disadvantage of splitting formulas is that of increasing communication amongst monitors.

In guarded sHML formulas, variables appear only as a sub-formula of a necessity formula.

We elevate \({{\mathrm{tr}}}\) to basic action sequences \(s\) in pointwise fashion, \({{\mathrm{tr}}}(s)\), where \({{\mathrm{tr}}}(\epsilon )=\epsilon \).

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

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

Armstrong J (2007) Programming Erlang. The Pragmatic Bookshelf, Armstrong

Bauer A, Falcone Y (2012) Decentralised LTL monitoring. In: Giannakopoulou D, Mry D (eds) FM. LNCS, vol 7436. Springer, pp 85–100

Bauer A, Leucker M, Schallhar C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20:14:1–14:64CrossRef

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.

Cao T-D, Phan-Quang T-T, Felix P, Castanet R (2010) Automated runtime verification for web services. In: ICWS. IEEE, pp 76–82

Carlsson R (2001) An introduction to Core Erlang. In: PLI’01 (Erlang Workshop)

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.

Francalanza A, Seychell A (2013) Synthesising correct concurrent runtime monitors in Erlang. Technical Report CS2013-01, University of Malta. https://www.cs.um.edu.mt/svrg/papers.html. Accessed Jan

20.

Francalanza A, Gauci A, Pace GJ (2013) Distributed System contract monitoring. JLAP 82(5–7):186–215MATHMathSciNet

21.

Francalanza A, Seychell A, Cassar I. DetectEr. https://bitbucket.org/casian/detecter2.0

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.

Kozen D (1983) Results on the propositional \(\mu \)-calculus. TCS 27:333–354MATHMathSciNetCrossRef

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.

Milner R, Parrow J, Walker D (1993) Modal logics for mobile processes. TCS 114:149–171MATHMathSciNetCrossRef

32.

Nicola RD, Hennessy MCB (1984) Testing equivalences for processes, TCS, pp 83–133

33.

Rensink A, Vogler W (2007) Fair testing. Inf Comput 205(2):125–198MATHMathSciNetCrossRef

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

Titel: Synthesising correct concurrent runtime monitors
verfasst von: Adrian Francalanza
Aldrin Seychell
Publikationsdatum: 01.06.2015
Verlag: Springer US
Erschienen in: Formal Methods in System Design / Ausgabe 3/2015
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-014-0217-9

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

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

Runtime verification with minimal intrusion through parallelism

Monitoring of temporal first-order properties with aggregations

The ins and outs of first-order runtime verification