Synchrone und asynchrone Interaktion in verteilten Systemen

• Antragstellerinnen / Antragsteller: Professorin Dr. Ursula Goltz; Professor Dr.-Ing. Uwe Nestmann; Dr. Kirstin Peters
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2010 bis 2018
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 167512345

• Erstellungsjahr: 2019

Zusammenfassung der Projektergebnisse

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.

Projektbezogene Publikationen (Auswahl)

• On characterising distributability. Logical Methods in Computer Science, 9(3), 2013
  Rob J. van Glabbeek, Ursula Goltz, and Jens-Wolfhard Schicke-Uffmann
  
• Full abstraction for expressiveness: history, myths and facts. Mathematical Structures in Computer Science, pages 1–16, 2014
  Danile Gorla and Uwe Nestmann
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• 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
  
• Keep it fair: Equivalence and composition. Journal of Logical and Algebraic Methods in Programming, 104:1 – 15, 2019
  Stephan Mennicke and Tobias Prehn