Synchronous and Asynchronous Interaction in Distributed Systems
Final Report Abstract
Wir konnten die in der ersten Projektphase begonnene Hierarchie stark ausbauen und die beiden Stränge stärker miteinander verknüpfen. Damit haben wir unser Hauptziel erreicht: Wir haben eine gute Grundlage geschaffen, aufgrund derer passende Modellierungssprachen für verteilte Systeme gewählt werden können. Die korrekte Wahl der Modellierungssprache ist wichtig, um zu garantieren, dass Evaluationen nicht durch versteckte Synchronisationsannahmen negativ beeinflusst werden und die ermittelten Ergebnisse tatsächlich der Realität entsprechen. Neben dem Unterschied zwischen uneingeschränkt verteilbaren und nicht-verteilbaren Klassen von Sprachen haben wir noch mehre Stufen von synchroner Interaktion identifiziert und analysiert. Damit können auch Modellierungswerkzeuge für unterschiedliche Anwendungsfälle mit abweichenden Systemvoraussetzungen richtig eingeordnet werden. Zu diesem Zweck haben wie eine ganze Reihe von Petrinetzklassen und Prozesskalkülen in die Hierarchie eingeordnet. Neben dieser Einordnung bestehender Modellierungssprachen liegt die größte Errungenschaft dieses Projektes jedoch in den identifizierten Interaktionsmustern und den entwickelten Beweistechniken. Wir haben untersucht, welche Faktoren für die Eignung von Modellierungssprachen überhaupt relevant sind und wie man beweist welche Sprachen diese Faktoren erfüllen oder verletzen. Die modell-unabhängige Charakterisierung der Interaktionsmuster erlaubt eine direkte Übertragung unserer Ergebnisse auf andere Modellierungswerkzeuge. Die Interaktionsmuster erlauben es schnell und einfach nach Formen von Synchronisation in Sprachen zu suchen und diese zu klassifizieren. Dies hilft uns, die Gründe für versteckte, unerwünschte Synchronisationen in Sprachen zu ergründen und diese Fehler in der Entwicklung neuer Sprachen oder deren Implementierung zu vermeiden. Die Einfachheit dieser Muster erlaubt es uns, auch intuitiv verständliche Erklärungen zu finden. Darüber hinaus haben wir uns auf verschiedenen Wegen der Frage genähert, welche Entwicklungen notwendig sind, um verteilte Algorithmen mit den untersuchten Modellierungsprachen effizient zu analysieren. Wir haben Fairnessannahmen und ihre Auswirkungen auf die Modellierungswerkzeuge untersucht, wir haben Multiparty Session Types um Fehlertoleranz erweitert und wir haben verschiedene Transformationen zwischen verteilten Sprachen erstellt, um deren positive Eigenschaften mit einander zu verbinden.
Publications
- On characterising distributability. Logical Methods in Computer Science, 9(3), 2013
Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke-Uffmann
(See online at https://doi.org/10.2168/LMCS-9(3:17)2013) - Full abstraction for expressiveness: history, myths and facts. Mathematical Structures in Computer Science, pages 1–16, 2014
Danile Gorla and Uwe Nestmann
(See online at https://doi.org/10.1017/S0960129514000279) - On the step branching time closure of free-choice petri nets. In Erika Ábrahám and Catuscia Palamidessi, editors, Formal Techniques for Distributed Objects, Components, and Systems, pages 232–248, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg
Stephan Mennicke, Jens-Wolfhard Schicke-Uffmann, and Ursula Goltz
(See online at https://doi.org/10.1007/978-3-662-43613-4_15) - Analysing and Comparing Encodability Criteria. In Silvia Crafa and Daniel Gebler, editors, Proceedings of EXPRESS/SOS, volume 190 of EPTCS, pages 46–60, 2015
Kirstin Peters and Rob van Glabbeek
(See online at https://doi.org/10.4204/EPTCS.190.4) - Encoding CSP into CCS. In Silvia Crafa and Daniel Gebler, editors, Proceedings of EXPRESS/SOS, volume 190 of EPTCS, pages 61–75, 2015
Meike Hatzel, Christoph Wagner, Kirstin Peters, and Uwe Nestmann
(See online at https://doi.org/10.4204/EPTCS.190.5) - Synchrony versus causality in distributed systems. Mathematical Structures in Computer Science, 26(8):1459–1498, 2016
Kirstin Peters, Jens-Wolfhard Schicke-Uffmann, Ursula Goltz, and Uwe Nestmann
(See online at https://doi.org/10.1017/S0960129514000644) - Session Types for Link Failures. In Ahmed Bouajjani and Alexandra Silva, editors, Proceedings of FORTE, volume 10321 of LNCS, pages 1–16, 2017
Manuel Adameit, Kirstin Peters, and Uwe Nestmann
(See online at https://doi.org/10.1007/978-3-319-60225-7_1) - On the Distributability of Mobile Ambients. In Jorge A. Pérez and Simone Tini, editors, Proceedings of EXPRESS/SOS, volume 276 of EPTCS, pages 104–121, 2018
Kirstin Peters and Uwe Nestmann
(See online at https://doi.org/10.4204/EPTCS.276.9) - Keep it fair: Equivalence and composition. Journal of Logical and Algebraic Methods in Programming, 104:1 – 15, 2019
Stephan Mennicke and Tobias Prehn
(See online at https://doi.org/10.1016/j.jlamp.2019.01.004)
