Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2015

01.06.2015

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

verfasst von: Romain Demangeon, Kohei Honda, Raymond Hu, Rumyana Neykova, Nobuko Yoshida

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
loading …

Abstract

The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, http://​www.​oceanobservatori​es.​org/​, JBoss Savara Project, http://​www.​jboss.​org/​savara) on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273–284, 2008), this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.
Nächster Artikel Synthesising correct concurrent runtime monitors

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
Anhänge
Nur mit Berechtigung zugänglich
Literatur
1.
Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták O, de Moor O, Sereni D, Sittampalam G, Tibble J (2005) Adding trace matching with free variables to aspectj. SIGPLAN Not 40(10):345–364CrossRef
2.
3.
Ancona D, Drossopoulou S, Mascardi V (2012) Automatic generation of self-monitoring mass from multiparty global session types in Jason. In: DALT. Springer, Berlin
4.
Avgustinov P, Tibble J, de Moor O (2007) Making trace monitors feasible. SIGPLAN Not 42(10):589–608CrossRef
5.
Baresi L, Ghezzi C, Guinea S (2004) Smart monitors for composed services. In: ICSOC. ACM, New York, pp 193–202
6.
Bettini L, et al. (2008) Global progress in dynamically interleaved multiparty sessions. In: CONCUR. LNCS, vol 5201. Springer, Berlin, pp 418–433
7.
Bocchi L, Chen T-C, Demangeon R, Honda K, Yoshida N (2013) Monitoring networks through multiparty session types. In: FMOODS. LNCS, vol 7892. Springer, Berlin, pp 50–65
8.
Bocchi L, Laneve C, Zavattaro G (2003) A calculus for long-running transactions. In: FMOODS. LNCS, vol 2884, Springer, Berlin, pp 124–138
9.
Boreale M, Bruni R, Nicola R, Loreti M (2008) Sessions and pipelines for structured service programming. In: Barthe G, Boer F (eds) FMOODS. LNCS, vol 5051. Springer, Berlin, pp 19–38
10.
Cambronero M-E et al (2011) Validation and verification of web services choreographies by using timed automata. J Log Algebraic Program 80(1):25–49MATHCrossRef
11.
Capecchi S, Giachino E, Yoshida N (2010) Global escape in multiparty session. In: FSTTCS. LNCS, vol 8, pp 338–351
12.
Carbone M (2009) Session-based choreography with exceptions. Electron Notes Theor Comput Sci 241:35–55CrossRef
13.
Carbone M, Honda K, Yoshida N (2008) Structured interactional exceptions in session types. In: CONCUR. LNCS, vol 5201. Springer, Berlin, pp 402–417
14.
15.
Chen T-C (2013) Theories for session-based governance for large-scale distributed systems. PhD thesis, Queen Mary, University of London, London
16.
Deniélou P-M, Yoshida N (2012) Multiparty session types meet communicating automata. In: ESOP. LNCS. Springer, Berlin, pp 194–213
17.
Gan Y, Chechik M, Nejati S, Bennett J, O’Farrell B, Waterhouse J (2007) Runtime monitoring of web service conversations. In: CASCON. ACM, New York, pp 42–57
18.
Ghezzi C, Guinea S (2007) Run-time monitoring in service-oriented architectures. In: Test and analysis of web services. Springer, Berlin, pp 237–264
19.
Hallé S, Bultan T, Hughes G, Alkhalaf M, Villemaire R (2010) Runtime verification of web service interface contracts. Computer 43(3):59–66CrossRef
20.
Honda K, Yoshida N, Carbone M (2008) Multiparty Asynchronous Session Types. In: POPL. ACM, New York, pp 273–284
21.
Hu R, Kouzapas D, Pernet O, Yoshida N, Honda K (2010) Type-safe eventful sessions in Java. In: ECOOP’10. LNCS, vol 6183. Springer-Verlag, New York, pp 329–353
22.
Hu R, Neykova R, Yoshida N, Demangeon R, Honda K (2013) Practical interruptible conversations—distributed dynamic verification with session types and python. In: RV. LNCS, vol 8174. Springer, Berlin, pp 130–148
23.
Jakšić S, Padovani L (2012) Exception handling for copyless messaging. In: PPDP. ACM, New York, pp 151–162
24.
25.
26.
Krüger IH, Meisinger M, Menarini M (2007) Runtime verification of interactions: from mscs to aspects. In: RV, RV. Springer-Verlag, Berlin, pp 63–74
27.
Krüger IH, Meisinger M, Menarini M (2010) Interaction-based runtime verification for systems of systems integration. J Log Comput 20(3):725–742CrossRef
28.
Lapadula A, Pugliese R, Tiezzi F (2007) A calculus for orchestration of web services. In: ESOP. LNCS, vol 4421. Springer, Berlin, pp 33–47
29.
30.
Li Z, Han J, Jin Y (2005) Pattern-based specification and validation of web services interaction properties. In: ICSOC’05, pp 73–86
31.
Li Z, Jin Y, Han J (2006) A runtime monitoring and validation framework for web service interactions. In: ASWEC, IEEE
32.
Minsky NH, Ungureanu V (2000) Law-governed interaction: a coordination and control mechanism for heterogeneous distributed systems. TOSEM 9:273–305CrossRef
33.
Ng N, Yoshida N, Honda K (2012) Multiparty session c: Safe parallel programming with message optimisation. In: TOOLS. LNCS, vol 7304. Springer, Berlin, pp 202–218
34.
35.
36.
37.
38.
Rubira CMF, Wu Z (1995) Fault tolerance in concurrent object-oriented software through coordinated error recovery. In: IEEE Computer Society, FTCS ’95, Washington, DC, pp 499–509
39.
Salaün G (2010) Analysis and verification of service interaction protocols - a brief survey. In: TAV-WEB. EPTCS, vol 35, pp 75–86
40.
41.
42.
43.
Tartanoglu F, Issarny V, Romanovsky A, Levy N (2003) Coordinated forward error recovery for compositeweb services. In: IEEE symposium on reliable distributed systems, pp 167–176
44.
Vieira HT, Caires L, Seco JC (2008) The conversation calculus: a model of service-oriented computation. In: ESOP. LNCS, vol 4960. Springer, Berlin, pp 269–283
45.
Xu J, Romanovsky A, Randell B (1998) Coordinated exception handling in distributed object systems: From model to system implementation. In: ICDCS, IEEE Computer Society, Washington, DC, pp 12–21
46.
Zhang W, Serban C, Minsky N (2007) Establishing global properties of multi-agent systems via local laws. In: E4MAS, pp 170–183
Metadaten
Titel
Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python
verfasst von
Romain Demangeon
Kohei Honda
Raymond Hu
Rumyana Neykova
Nobuko Yoshida
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-0218-8

Weitere Artikel der Ausgabe 3/2015

Formal Methods in System Design 3/2015 Zur Ausgabe

OriginalPaper

The ins and outs of first-order runtime verification

OriginalPaper

Monitoring of temporal first-order properties with aggregations

OriginalPaper

Runtime verification with minimal intrusion through parallelism

OriginalPaper

Synthesising correct concurrent runtime monitors

Premium Partner

    Bildnachweise