nach oben

Erschienen in:

2021 | OriginalPaper | Buchkapitel

Better Late Than Never or: Verifying Asynchronous Components at Runtime

verfasst von : Duncan Paul Attard, Luca Aceto, Antonis Achilleos, Adrian Francalanza, Anna Ingólfsdóttir, Karoliina Lehtinen

Erschienen in: Formal Techniques for Distributed Objects, Components, and Systems

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

This paper presents detectEr, a runtime verification tool for monitoring asynchronous component systems. The tool synthesises executable monitors from properties expressed in terms of the safety fragment of the modal \(\mu \)-calculus. In this paper, we show how a number of useful properties can be flexibly runtime verified via the three forms of instrumentation—inline, outline, and offline—offered by detectEr to cater for specific system set-up constraints.

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

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

Vorheriges Kapitel Formal Verification of HotStuff

Nächstes Kapitel Tutorial: Designing Distributed Software in mCRL2

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: Monitoring for silent actions. In: FSTTCS. LIPIcs, vol. 93, pp. 7:1–7:14 (2017)

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A.: A framework for parameterized monitorability. In: Baier, C., Dal Lago, U. (eds.) FoSSaCS 2018. LNCS, vol. 10803, pp. 203–220. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89366-2_11CrossRef

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: On the complexity of determinizing monitors. In: Carayol, A., Nicaud, C. (eds.) CIAA 2017. LNCS, vol. 10329, pp. 1–13. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-60134-2_1CrossRefMATH

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Kjartansson, S.Ö.: Determinizing monitors for HML with recursion. JLAMP 111, 100515 (2020)MathSciNetMATH

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1–52:29 (2019)CrossRef

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: An operational guide to monitorability with applications to regular properties. Softw. Syst. Model. 20(2), 335–361 (2021). https://doi.org/10.1007/s10270-020-00860-zCrossRef

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: The best a monitor can do. In: CSL. LIPIcs, vol. 183, pp. 7:1–7:23 (2021)

Aceto, L., Attard, D.P., Francalanza, A., Ingólfsdóttir, A.: A choreographed outline instrumentation algorithm for asynchronous components. CoRR abs/2104.09433 (2021)

Aceto, L., Attard, D.P., Francalanza, A., Ingólfsdóttir, A.: On benchmarking for concurrent runtime verification. FASE 2021. LNCS, vol. 12649, pp. 3–23. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71500-7_1CrossRef

10.

Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On runtime enforcement via suppressions. In: CONCUR. LIPIcs, vol. 118, pp. 34:1–34:17 (2018)

11.

Aceto, L., Ingólfsdóttir, A.: Testing Hennessy-Milner logic with recursion. In: Thomas, W. (ed.) FoSSaCS 1999. LNCS, vol. 1578, pp. 41–55. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49019-1_4CrossRef

12.

Agha, G., Mason, I.A., Smith, S.F., Talcott, C.L.: A foundation for actor computation. JFP 7(1), 1–72 (1997)MathSciNetMATH

13.

Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1987). https://doi.org/10.1007/BF01782772CrossRefMATH

14.

Andersen, J.R., et al.: CAAL: concurrency workbench, Aalborg edition. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 573–582. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_33CrossRef

15.

Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf (2007)

16.

ASF: Log4J 2 (2021). https://logging.apache.org/log4j/2.x

17.

Attard, D.P., Francalanza, A.: A monitoring tool for a branching-time logic. In: Falcone, Y., Sánchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 473–481. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46982-9_31CrossRef

18.

Attard, D.P., Francalanza, A.: Trace partitioning and local monitoring for asynchronous components. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 219–235. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66197-1_14CrossRef

19.

Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH

20.

Bartocci, E., Falcone, Y., Francalanza, A., Reger, G.: Introduction to runtime verification. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 1–33. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_1CrossRef

21.

Basho: Lager (2021). https://github.com/basho/lager

22.

Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21–39. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_2CrossRef

23.

Cantrill, B.: Hidden in plain sight. ACM Queue 4(1), 26–36 (2006)CrossRef

24.

Cassar, I., Francalanza, A., Attard, D.P., Aceto, L., Ingólfsdóttir, A.: A suite of monitoring tools for Erlang. In: RV-CuBES, vol. 3, pp. 41–47. Kalpa Publications in Computing (2017)

25.

Cassar, I., Francalanza, A., Said, S.: Improving runtime overheads for detectEr. In: FESCA. EPTCS, vol. 178, pp. 1–8 (2015)

26.

Cesarini, F., Thompson, S.: Erlang Programming: A Concurrent Approach to Software Development. O’Reilly Media, Sebastopol (2009)MATH

27.

Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-35746-6_1CrossRef

28.

Desnoyers, M., Dagenais, M.R.: The LTTng tracer: a low impact performance and behavior monitor for GNU/Linux. Technical report, École Polytechnique de Montréal (2006)

29.

Dijkstra, E.W.: Chapter I: notes on structured programming, p. 1–82. Academic Press Ltd. (1972)

30.

Eclipse/IBM: Openj9 (2021). https://www.eclipse.org/openj9

31.

Erlingsson, Ú.: The inlined reference monitor approach to security policy enforcement. Ph.D. thesis, Cornell University (2004)

32.

Erlingsson, Ú., Schneider, F.B.: SASI enforcement of security policies: a retrospective. In: NSPW, pp. 87–95 (1999)

33.

Facorro, J.: Clojerl language (2021). http://clojerl.org

34.

Falcone, Y., Krstić, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) RV 2018. LNCS, vol. 11237, pp. 241–262. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03769-7_14CrossRef

35.

Francalanza, A.: Consistently-detecting monitors. In: CONCUR. LIPIcs, vol. 85, pp. 8:1–8:19 (2017)

36.

Francalanza, A.: A theory of monitors. Inf. Comput. 104704 (2021). https://doi.org/10.1016/j.ic.2021.104704

37.

Francalanza, A., et al.: A foundation for runtime monitoring. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 8–29. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67531-2_2CrossRef

38.

Francalanza, A., Aceto, L., Ingolfsdottir, A.: On verifying Hennessy-Milner logic with recursion at runtime. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 71–86. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23820-3_5CrossRef

39.

Francalanza, A., Aceto, L., Ingólfsdóttir, A.: Monitorability for the Hennessy-Milner logic with recursion. FMSD 51(1), 87–116 (2017). https://doi.org/10.1007/s10703-017-0273-zCrossRefMATH

40.

Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. Int. J. Softw. Tools Technol. Transf. 15(2), 89–107 (2013). https://doi.org/10.1007/s10009-012-0244-zCrossRefMATH

41.

Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)MATH

42.

Jurić, S.: Elixir in Action. Manning (2019)

43.

Kozen, D.: Results on the propositional \(\mu \)-calculus. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 348–359. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0012782CrossRef

44.

Larsen, K.G.: Proof systems for satisfiability in Hennessy-Milner logic with recursion. TCS 72(2&3), 265–288 (1990)MathSciNetCrossRef

45.

Leucker, M., Schallhart, C.: A brief account of runtime verification. JLAP 78(5), 293–303 (2009)MATH

46.

Loy, M., Niemeyer, P., Leuck, D.: Learning Java: An Introduction to Real-World Programming with Java. O’Reilly Media, Sebastopol (2020)

47.

Myers, G.J., Sandler, C., Badgett, T.: The Art of Software Testing. Wiley, Hoboken (2011)

48.

Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)MATH

49.

Python: Logging Facility for Python (2021). https://docs.python.org/3/library/logging.html

Titel: Better Late Than Never or: Verifying Asynchronous Components at Runtime
verfasst von: Duncan Paul Attard
Luca Aceto
Antonis Achilleos
Adrian Francalanza
Anna Ingólfsdóttir
Karoliina Lehtinen
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-78088-3

Electronic ISBN: 978-3-030-78089-0

Copyright-Jahr: 2021
DOI: https://doi.org/10.1007/978-3-030-78089-0_14

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

Springer Professional "Wirtschaft"