Synthesis and Analysis of Component Connectors (SYANCO)
Final Report Abstract
Im Rahmen des SYANCO-Projektes haben wir verschiedene Aspekte der Koordinierung von Komponenten durch Konnektoren und Netzwerke von Kanälen unter dem Blickwinkel der formalen Analyse untersucht. Als Grundvoraussetzung für die formale Analyse haben wir Modellierungssprachen sowohl für die automatenbasierte Beschreibung von Komponenten, Kanälen und Konnektoren als auch für den skriptgesteuerten, kompositionellen Aufbau von komplexen Konnektoren und Systemen entwickelt. Als gemeinsame operationelle Semantik dienen dabei Constraint Automaten, deren Transitionsbeschriftungen die mögliche Interaktion zwischen den Komponenten und Konnektoren abbilden. Für die formale Analyse von Constraint Automaten haben wir passende Logiken entwickelt, die zum einen hinreichend ausdrucksstark für die Formalisierung der relevanten Eigenschaften sind, aber auch den Einsatz effizienter Analysealgorithmen erlauben. Wir haben dazu Standardlogiken zur Spezifikation paralleler Systeme um spezielle Modalitäten zur Darstellung der Interaktion erweitert und passende Model Checking Algorithmen entwickelt. Die entwickelten Modellierungssprachen und Analysealgorithmen haben wir im Tool Vereofy implementiert. Dabei wird das Model Checking für Linearzeit- und Branching Time-Eigenschaften, jeweils unter Berücksichtigung der Interaktionen der Komponenten und Konnektoren, unterstützt. Vereofy kann dabei in die Extensible Coordination Tools unserer niederländischen Partner integriert werden, wodurch unter anderem eine graphische Modellierung der Konnektoren als Reo-Netzwerke unterstützt wird. Vereofy wurde von uns im Rahmen von mehreren größeren Fallstudien eingesetzt, um sowohl den Modellierungansatz als auch die Effizienz der von uns gewählten Algorithmen zu evaluieren. Die von uns entwickelte alternierende Logik ASL wird ebenso unterstützt, eine Erweiterung von Alternating Time Logic um Streamoperatoren. ASL liegt eine Interpretation unseres Automatenmodells als Mehrparteienspiel zugrunde. Sie ermöglicht Aussagen zur Existenz von Strategien für (Koalitionen von) Komponenten, um gewisse globale Eigenschaften des Gesamtsystems zu erzwingen. Diese Strategien können wiederum als Automaten synthetisiert werden. ASL-Formeln können auch zur Formalisierung von Kompatibilitätseigenschaften eingesetzt werden. Weiterhin haben wir ein algorithmisches Framework entwickelt, das eine kompositionelle Synthese von Konnektoren erlaubt. Mehrere zu erfüllende Zielvorgaben können dabei iterativ abgearbeitet werden, da die erzeugten Controller so allgemein wie möglich sind. Vereofy stellt dabei für diese und weitergehende Forschungsvorhaben die nötige Infrastruktur bereit.
