nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)

verfasst von : Christian Bartolo Burlò, Adrian Francalanza, Alceste Scalas

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

We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one endpoint is statically checked, and the other endpoint is dynamically checked by a monitor acting as an intermediary between typed and untyped components. We outline our theory, and illustrate a tool that automatically synthesises type-checked session monitors, based on the Scala language and its session programming library (lchannels).

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 Typechecking Java Protocols with [St]Mungo

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. PACMPL 3(POPL), 1–29 (2019). https://doi.org/10.1145/3290365CrossRef

Aceto, L., Achilleos, A., Francalanza, A., Ingólfsdóttir, A., Lehtinen, K.: An operational guide to monitorability. In: Ölveczky, P.C., Salaün, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 433–453. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30446-1_23CrossRef

Aceto, L., Cassar, I., Francalanza, A., Ingólfsdóttir, A.: On runtime enforcement via suppressions. In: CONCUR, LIPIcs, vol. 118. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.34

Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2–3), 95–230 (2016). https://doi.org/10.1561/2500000031CrossRef

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

Bocchi, L., Chen, T.-C., Demangeon, R., Honda, K., Yoshida, N.: Monitoring networks through multiparty session types. In: Beyer, D., Boreale, M. (eds.) FMOODS/FORTE - 2013. LNCS, vol. 7892, pp. 50–65. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38592-6_5CrossRef

Burlò, C.B., Francalanza, A., Scalas, A.: STMonitor implementation (February 2020). https://github.com/chrisbartoloburlo/stmonitor

Cesarini, F., Thompson, S.: ERLANG Programming, 1st edn. O’Reilly Media Inc., Sebastopol (2009)MATH

Dardha, O., Giachino, E., Sangiorgi, D.: Session types revisited. Inf. Comput. 256, 253–286 (2017). https://doi.org/10.1016/j.ic.2017.06.002MathSciNetCrossRefMATH

10.

Demangeon, R., Honda, K., Hu, R., Neykova, R., Yoshida, N.: Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python. Form. Methods Syst. Des. 46(3), 197–225 (2014). https://doi.org/10.1007/s10703-014-0218-8CrossRefMATH

11.

Francalanza, A., Aceto, L., Ingolfsdottir, A.: Monitorability for the Hennessy–Milner logic with recursion. Form. Methods Syst. Des. 51(1), 87–116 (2017). https://doi.org/10.1007/s10703-017-0273-zCrossRefMATH

12.

Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509–523. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57208-2_35CrossRef

13.

Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053567CrossRef

14.

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL. ACM (2008). https://doi.org/10.1145/1328438.1328472. Full version in [15]

15.

Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 1–67 (2016). https://doi.org/10.1145/2827695MathSciNetCrossRefMATH

16.

Hüttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 1–36 (2016). https://doi.org/10.1145/2873052CrossRef

17.

Jia, L., Gommerstadt, H., Pfenning, F.: Monitors and blame assignment for higher-order session types. In: POPL. ACM (2016). https://doi.org/10.1145/2837614.2837662

18.

Neykova, R., Hu, R., Yoshida, N., Abdeljallal, F.: A session type provider: Compile-time API generation of distributed protocols with refinements in f#. In: Proceedings of the 27th International Conference on Compiler Construction, CC 2018. ACM (2018). https://doi.org/10.1145/3178372.3179495

19.

Neykova, R., Yoshida, N.: Let it recover: multiparty protocol-induced recovery. In: Proceedings of the 26th International Conference on Compiler Construction. ACM (2017). https://doi.org/10.1145/3033019.3033031

20.

OAuth Working Group: RFC 6749: OAuth 2.0 framework (2012). http://tools.ietf.org/html/rfc6749

21.

Scalas, A.: lchannels (2017). https://alcestes.github.io/lchannels

22.

Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming. In: ECOOP, Leibniz International Proceedings in Informatics (LIPIcs), vol. 74. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2017). https://doi.org/10.4230/LIPIcs.ECOOP.2017.24

23.

Scalas, A., Dardha, O., Hu, R., Yoshida, N.: A linear decomposition of multiparty sessions for safe distributed programming (artifact). DARTS 3(2) (2017). https://doi.org/10.4230/DARTS.3.2.3

24.

Scalas, A., Yoshida, N.: Lightweight session programming in scala. In: ECOOP, LIPIcs, vol. 56. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016). https://doi.org/10.4230/LIPIcs.ECOOP.2016.21

25.

Scalas, A., Yoshida, N.: Lightweight session programming in scala (artifact). DARTS 2(1) (2016). https://doi.org/10.4230/DARTS.2.1.11

26.

Scribble Homepage (2020). http://www.scribble.org

27.

Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Maritsas, D., Philokyprou, G., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol. 817, pp. 398–413. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58184-7_118CrossRef

28.

Yoshida, N., Hu, R., Neykova, R., Ng, N.: The scribble protocol language. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 22–41. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-05119-2_3CrossRef

Titel: Towards a Hybrid Verification Methodology for Communication Protocols (Short Paper)
verfasst von: Christian Bartolo Burlò
Adrian Francalanza
Alceste Scalas
Verlag: Springer International Publishing
Buch: Formal Techniques for Distributed Objects, Components, and Systems
Print ISBN: 978-3-030-50085-6

Electronic ISBN: 978-3-030-50086-3

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-50086-3_13

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"