nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Realisability of Choreographies

verfasst von : Klaus-Dieter Schewe, Yamine Aït-Ameur, Sarah Benyagoub

Erschienen in: Foundations of Information and Knowledge 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

Choreographies prescribe the rendez-vous synchronisation of messages in a system of communicating finite state machines. Such a system is called realisable, if the traces of the prescribed communication coincide with those of the asynchronous system of peers, where the communication channels either use FIFO queues or multiset mailboxes. In this paper we provide two necessary conditions for synchronisability and hence for realisability of communication choreographies. We show that both conditions together are sufficient. A simple consequence is that realisability in the presence of a choreography becomes decidable. The conditions permit realisable choreographies to be obtained by means of composition, and then choreographies can be further refined into concurrent systems of communicating machines.

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 Logic-Based Approach to Incremental Monitoring and Optimization on Strongly Distributed Data Streams

Nächstes Kapitel Schema Optimisation Instead of (Local) Normalisation

Note that the automata defined in the next two definitions are not FSMs, strictly speaking, as there may be infinitely many states. Nonetheless, languages accepted by these automata can be defined analogously to FSMs.

As we will see, \(\epsilon \)-transitions are not needed, but they come in handy in proofs.

In fact, all counter-examples in [12] to previously claimed decidability results are P2P systems that are not choreography-defined.

As the theory is based on FSMs, there is no possibility to express parallelism.

Basu, S., Bultan, T.: Choreography conformance via synchronizability. In: Srinivasan, S., et al. (eds.) Proceedings of the 20th International Conference on World Wide Web (WWW 2011), pp. 795–804. ACM (2011)

Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci. 656, 60–75 (2016)MathSciNetCrossRef

Basu, S., Bultan, T., Ouederni, M.: Deciding choreography realizability. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012), pp. 191–202. ACM (2012)

Benyagoub, S., Aït-Ameur, Y., Ouederni, M., Mashkoor, A., Medeghri, A.: Formal design of scalable conversation protocols using Event-B: validation, experiments and benchmarks. J. Softw. Evol. Process (2019, to appear)

Benyagoub, S., Ouederni, M., Aït-Ameur, Y., Mashkoor, A.: Incremental construction of realizable choreographies. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 1–19. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_1CrossRef

Benyagoub, S., Ouederni, M., Singh, N.K., Ait-Ameur, Y.: Correct-by-construction evolution of realisable conversation protocols. In: Bellatreche, L., Pastor, Ó., Almendros Jiménez, J.M., Aït-Ameur, Y. (eds.) MEDI 2016. LNCS, vol. 9893, pp. 260–273. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45547-1_21CrossRef

Börger, E., Schewe, K.-D.: Concurrent abstract state machines. Acta Informatica 53(5), 469–492 (2016)MathSciNetCrossRef

Börger, E., Schewe, K.-D.: Communication in abstract state machines. J. UCS 23(2), 129–145 (2017)MathSciNet

Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)MathSciNetCrossRef

10.

Chambart, P., Schnoebelen, P.: Mixing lossy and perfect fifo channels. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 340–355. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85361-9_28CrossRef

11.

Clemente, L., Herbreteau, F., Sutre, G.: Decidable topologies for communicating automata with FIFO and bag channels. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 281–296. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44584-6_20CrossRef

12.

Finkel, A., Lozes, É.: Synchronizability of communicating finite state machines is not decidable. In: Chatzigiannakis, I., et al. (eds.) 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). LIPIcs, vol. 80, pp. 122:1–122:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

13.

Schewe, K.-D.: Extensions to hybrid Event-B to support concurrency in cyber-physical systems. In: Abdelwahed, E.H., Bellatreche, L., Golfarelli, M., Méry, D., Ordonez, C. (eds.) MEDI 2018. LNCS, vol. 11163, pp. 418–433. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00856-7_28CrossRef

14.

Zoubeyr, F., Aït-Ameur, Y., Ouederni, M., Tari, K.: A correct-by-construction model for asynchronously communicating systems. STTT 19(4), 465–485 (2017)CrossRef

Titel: Realisability of Choreographies
verfasst von: Klaus-Dieter Schewe
Yamine Aït-Ameur
Sarah Benyagoub
Verlag: Springer International Publishing
Buch: Foundations of Information and Knowledge Systems
Print ISBN: 978-3-030-39950-4

Electronic ISBN: 978-3-030-39951-1

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39951-1_16

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"