Automatische Synthese Verteilter und Parametrisierter Systeme

• Antragsteller: Privatdozent Dr.-Ing. Swen Jacobs
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2015 bis 2019
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 266796805

Das Ziel von Synthesemethoden ist die automatische Konstruktion von Systemen, die eine gegebene formale Spezifikation erfüllen, und somit dem Designer die zeitraubende und fehleranfällige Aufgabe abzunehmen, Programmdetails von Hand zu implementieren. Trotz dieser Vorteile werden formale Methoden, die Korrektheit a priori garantieren, heute kaum im Designprozess eingesetzt, im Gegensatz zu a posteriori-Methoden wie der Verifikation. Ein Grund dafür liegt in der Komplexität der benötigten Berechnungen, die noch höher ist als bei derVerifikation. Trotz dieser Hindernisse hat die Forschung im Bereich der Synthese in den letzten Jahren verstärkt neue Impulse erhalten, befeuert durch erstaunliche Fortschritte bei automatischen Beweismethoden.Ein entscheidendes Forschungsgebiet, das bisher relativ wenig Beachtung gefunden hat, ist die Synthese von verteilten Systemen, die aus mehreren nebenläufigen Prozessen bestehen. Die wachsende Bedeutung solcher Systeme, wie Mehrkern-Prozessoren und kommunizierende eingebettete Systeme oder Web-Dienste, wird bisher nicht begleitet von einem entsprechend wachsenden Forschungsaufwand für Methoden zur Synthese dieser Systeme. Dies ist umso erstaunlicher, da Synthese für solche Systeme besonders wichtig ist, denn die vielfältigen Wechselwirkungen zwischen einzelnen Komponenten des Systems machen es besonders schwer, korrekte Systeme von Hand zu entwickeln.Dieser Antrag zielt darauf ab, neue Methoden und Werkzeuge für die automatische Synthese von verteilten und parametrisierten Systemen zu entwickeln, wie etwa Kommunikationsprotokolle mit einer gegebenen oder parametrischen Anzahl von Teilnehmern. Um dies zu erreichen, werden wir Ansätze für die Verifikation von verteilten und parametrisierten Systemen untersuchen, und diese Ansätze so erweitern, dass sie zur Lösung des schwierigeren Problems der automatischen Synthese genutzt werden können. Dies beinhaltet die Entwicklung von effizienten Methoden für die Synthese von verteilten Systemen mit endlichem Zustandsraum, von Reduktionen des parametrisierten Syntheseproblems auf das verteilte Syntheseproblem, und von Methoden für die Synthese von verteilten Systemen mit unendlichem Zustandsraum.Das Ziel des Projekts ist es, neue grundlegende Methoden für die Synthese zu entwickeln, und die entstehenden Ansätze an kleinen bis mittelgroßen Fallstudien zu testen. Als Benchmark-Fallstudien werden wir unter anderem den ARM AMBA Bus Controller und Cache Coherence Protokolle betrachten. Der AMBA Controller wurde bereits vorher als Benchmark für Synthesewerkzeuge benutzt, ist für den allgemeinen Fall mit einer parametrischen Anzahl von Komponenten aber ungelöst. Cache Coherence Protokolle sind eine technisch herausfordernde Fallstudie, da in diesem Fall nicht nur eine korrekte, sondern auch eine effiziente Implementierung synthetisiert werden soll. Wir werden Methoden entwickeln, die das parametrisierte Syntheseproblem für diese und komplexere Fallstudien lösen können.

• DFG-Verfahren: Sachbeihilfen