Kompositionale Verifikation von Netzwerkalgorithmen und reaktiven Systemen

点击翻译按钮获取中文摘要

Informationstechnische Aufgaben werden zunehmend mit Hilfe verteilter Rechnernetze gelöst. Durch die Interaktion mit seiner Umgebung realisiert ein Rechnernetz ein reaktives System. Die auf einem Rechnernetz ablaufenden Algorithmen sind verteilt. Die Korrektheit solcher Algorithmen ist mit herkömmlichen Mitteln oftmals schwer oder gar nicht nachweisbar. Ein verteilter Algorithmus besteht oft aus Komponenten, die vergleichsweise einfach zu verifizieren sind. Allerdings sind sie meist auf komplizierte Art mit ihrer Umgebung verwoben. In diesem Projekt werden neuartige Verfahren entwickelt, um Algorithmen so aus einfachen Algorithmen zu komponieren, daß ihre entscheidenden Eigenschaften aus Eigenschaften der Komponenten ableitbar sind. Die resultierenden Verfahren werden verwendet, um einige Algorithmen zu verifizieren, deren Korrektheit bisher nicht überzeugend nachweisbar ist. Die neuen Verfahren verwenden neue Sichtweisen der Darstellung verteilter Algorithmen, die entsprechende neue Beweismethoden nach sich ziehen.