Parametrische Synthese Nebenläufiger und Verteilter Systeme

Programmsynthese ist ein Forschungszweig im Gebiet der Formalen Methoden. Synthesemethoden ermöglichen die automatische Konstruktion von Systemen aus formalen Spezifikationen, und nehmen somit dem Designer die zeitraubende und fehleranfällige Aufgabe ab, Programmdetails von Hand zu implementieren. Bei nebenläufigen und verteilten Systemen erschwert das Zusammenspiel der verschiedenen Komponenten die Konstruktion eines korrekten Systems zusätzlich, so dass Synthesemethoden in diesem Fall besonders vorteilhaft sind. Trotz dieser potentiellen Vorteile sind solche Methoden bisher noch weitgehend unerforscht. Dieser Antrag zielt darauf ab, neue Methoden für die automatische Synthese von nebenläufigen und verteilten Systemen mit einer parametrischen Anzahl von Komponenten zu entwickeln. Die Ziele des Projekts sind die Verbesserung unseres Verständnisses des Syntheseproblems, sowie die Entwicklung von Synthesewerkzeugen für diese Klasse von Systemen. Dazu werden wir Erkenntnisse aus den Forschungsbereichen der Verifikation und Synthese von verschiedenen Klassen von Systemen zusammenführen. Wir planen in folgende konkrete Probleme zu erforschen: (1)die Entwicklung effizienter Syntheseprozeduren, die existierende Verifikations- und Synthesemethoden erweitern und optimieren, um automatisch korrekte verteilte Systeme mit einer festen Anzahl von Komponenten zu generieren; (2)die Erweiterung der Anwendbarkeit unseres existierenden Ansatzes für Parametrisierte Synthese, der Entscheidbarkeitsresultate aus der Parametrisierten Verifikation benutzt um das parametrisierte Syntheseproblem auf ein Syntheseproblem mit einer festen Anzahl von Komponenten zu reduzieren. Methoden aus (1) können dann genutzt werden, um das reduzierte Problem zu lösen; (3)die Entwicklung von Syntheseansätzen, die abstraktionsbasierte Verifikationstechniken (für System emit unentscheidbarem Verifikationsproblem) mit Syntheseansätzen kombinieren, die durch fehlgeschlagene Verifikationsversuche gesteuert werden. Hier werden Methoden aus (1) als Sub- Prozeduren genutzt; (4)die Demonstration der Anwendbarkeit der resultierenden Methoden auf herausfordernden Fallstudien, insbesondere der Synthese von Cache Coherence Protokollen.