Certifying Algorithms for Interactive Components and Distributed Systems
Final Report Abstract
Wir haben eine Methode vorgestellt, das Konzept zertifizierender sequentieller Algorithmen auf terminierende verteilte Algorithmen zu übertragen. Die Übertragung resultiert in einer Klasse zertifizierender verteilter Algorithmen, • die ihr verteiltes Eingabe-Ausgabe-Paar verifizieren, • einen verteilten Zeugen mit jeder Ausgabe berechnen und • ein verteilbares Zeugenpradikat besitzen,• das wiederum durch einen verteilten Checker entschieden wird. Eine allgemeine Herausforderung verteilter Algorithmen ist, dass jede Komponente unvollständiges Wissen über das Netzwerk, sowie eine verteilte Eingabe und Ausgabe hat. Diese Herausforderung führt für verteilte Zeugen zum Problem der Konsistenz. Jede Komponente berechnet einen Teilzeugen. Dabei weiß sie nicht, ob dieser mit den Teilzeugen der anderen Komponenten konsistent ist. Wir haben das Problem der Konsistenz untersucht und mit zusammenhängenden Zeugen eine allgemeine Konstruktion für Zeugen aufgezeigt, deren Konsistenz lokal in den Nachbarschaften eines Netzwerks prüfbar ist. Des Weiteren haben wir verteilbare Zeugenpradikate eingeführt und untersucht. Ein verteilbares Prädikat kann entschieden werden, indem jeder Teilchecker unabhängig lokale Prädikate für seine Komponenten entscheidet. Durch die Einführung verteilbarer Zeugenpradikate haben wir eine verteilte Laufzeitverifikation erreicht. Wir haben uns mit der Herausforderung der Kommunikation in Netzwerken im Kontext von Checkern beschäftigt. Wir haben gezeigt, dass ein sequentieller Checker nicht zu den Gegebenheiten eines Netzwerks passt und deshalb eine verteilte Architektur für Checker entworfen. Die Kommunikation für die Aufgabe der Evaluation eines verteilbaren Zeugenprädikats läuft immer nach dem gleichen Schema ab. Für die Aufgabe der Konsistenzprüfung haben wir zum einen eine Konsistenzprüfung für beliebige Zeugen entwickelt, für die im gesamten Netzwerk Kommunikation anfällt und zum anderen eine lokale Konsistenzprüfung zusammenhängender Zeugen für die nur in Nachbarschaften kommuniziert wird. Anhand der industriellen Fallstudie der zertifizierenden verteilten Auktion für Transportroboter in einer Fabrik haben wir uns zum einen mit Multi-Agenten-Systemen beschäftigt und zum anderen den Einsatz virtueller Netzwerke zur Reduktion der Invasivität des Checkers untersucht. Wir konnten anhand der Fallstudie nicht nur eine Reduktion aufzeigen, sondern die Ergebnisse sind auch auf jedes Netzwerk übertragbar, dessen Topologie bekannt ist. Wir haben zertifizierende verteilte Algorithmen aus einem softwaretechnischen Blickwinkel heraus betrachtet. Zur Analyse der Kerngedanken Verteiltheit, Gleichheit und Lokalität bei der Zertifizierung haben wir zentralisierte Zeugen, gleichverteilte Zeugen und beschränkte Zeugen untersucht. Wir haben außerdem Kriterien zur Güte einer Zertifizierung, sowie Entwurfsmuster fur zertifizierende verteilte Algorithmen entwickelt. Wir haben für eine Übertragung des Konzepts zertifizierender Algorithmen auf verteilte Algorithmen zwei Ziele motiviert. Ein Ziel war, das Konzept so zu übertragen, dass es nah am ursprünglichen Konzept sequentieller Algorithmen ist. Wir haben uns bei dieser Übertragung auf terminierende verteilte Algorithmen beschränkt, wodurch uns eine direktere Übertragung gelang. Zertifizierende verteilte Algorithmen sind ein Spezialfall zertifizierender sequentieller Algorithmen, mit vergleichbaren Rollen für Zeuge, Zeugenpradikat und Checker. Ein weiteres Ziel war, das Konzept so zu übertragen, dass es zu den Gegebenheiten eines verteilten Systems passt. Wir denken, das uns dies gelungen ist, denn Zeugen werden verteilt berechnet und Zeugenprädikate verteilt verifiziert. Wir denken außerdem, dass die verschiedenen Fallstudien zeigen, dass die entwickelte Klasse zertifizierender verteilter Algorithmen diesem Anspruch gerecht wird. Unsere Methode der Übertragung resultiert in einer verteilten Laufzeitverifikation – einem Gebiet, zu dem es bisher nur wenige Arbeiten gibt und das ein aktuelles Forschungsgebiet darstellt. Wir haben eine Methodik zur formalen Instanzverifikation für zertifizierende verteilte Algorithmen entwickelt und diese in einem Framework für den Beweisassistenten COQ umgesetzt. Verifizierte Checker können dabei auf einem realen Netzwerk laufen und sogar verifiziert fehlertolerant gestaltet werden. Wir haben das Framework an drei Fallstudien illustriert. Des Weiteren haben wir die lokale und die allgemeine Konsistenzprüfung fur das Framework in COQ implementiert.
Publications
-
“Certification of Distributed Algorithms Solving Problems with Optimal Substructure”. In: Software Engineering and Formal Methods. Hrsg. von R. Calinescu und B. Rumpe. Springer International Publishing, 2015, S. 190–195
K. Völlinger und W. Reisig
-
“Verifying a class of certifying distributed programs”. In: NASA Formal Methods Symposium. Springer. 2017, S. 373–388
K. Völlinger und S. Akili
-
“Verifying the output of a distributed algorithm using certification”. In: International Conference on Runtime Verification. Springer. 2017, S. 424–430
K. Völlinger
-
“On a verification framework for certifying distributed algorithms: distributed checking and consistency”. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems. Springer. 2018, S. 161–18
K. Völlinger und S. Akili
-
“Case study on certifying distributed algorithms: reducing intrusiveness”. In: International Conference on Fundamentals of Software Engineering. Springer. 2019, S. 179–185
S. Akili und K. Völlinger
-
“On Certifying Distributed Algorithms: Problem of Local Correctness”. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems. Springer. 2019, S. 281–288
K. Völlinger
-
Zertifizierende verteilte Algorithmen. Humboldt-Universitat zu Berlin. 2020
K. Völlinger
