Moderne Graphalgorithmen Techniken zur Formalverifikation

Fehlerlose Software und Hardware zu entwickeln ist eine der großen Herausforderungen der Informatik. Subtile Fehler in komplexen Systemen können viele Probleme verursachen. Beispiele hierfür sind der kostspielige Pentium-Chip Fehler oder Softwarefehler, die zum Absturz von Laptops und von Weltraumraketen, wie der Ariane 5, führten. Im Forschungsgebiet der computer-gestützten Verifikation werden automatische Techniken entwickelt, die die Korrektheit von Systemen formal analysieren und in der Entdeckung von subtilen Fehler helfen. Das geschieht wie folgt: Zuerst wird ein mathematisches Modell des Systems entwickelt. Üblicherweise ist dieses Model eine Erweiterung eines Graphmodells. In diesen Graphmodellen werden Systemzustände durch Knoten und Systemübergänge durch Kanten repräsentiert. Pfade im Graph entsprechen dem Verhalten eines Systems. Das mathematische Model wird dann mit einer Spezifikation, die das gewünschte Verhalten des Systems beschreibt, verglichen. Daher sind automatische Verifikationstechniken nichts anderes als Algorithmen zur Analyse der Eigenschaften von Graphen. Da Software und Hardware immer komplexer und größer werden, steigt auch die Bearbeitungszeit der existierenden Verifikationstools rasant. Um den Einsatz der Verifikationstools weiter zu gewährleisten, müssen daher dringend schnellere Verifikationstechniken entwickelt werden. Gleichzeitig haben neue algorithmische Techniken graphalgorithmische Probleme in anderen Gebieten stark verbessert. Sie werden aber noch nicht in der Verifikation benützt. Unser Ziel ist es daher, diese neuen algorithmischen Techniken zur Verbeschleunigung von Verifikationsalgorithmen einzusetzen. Die meisten Verifikationstools benützen die gleichen zentralen Graphalgorithmen. Für viele dieser zentralen Probleme liegen die oberen und unteren Laufzeitschranken noch weit auseinander, d.h. die Laufzeit der Probleme ist noch nicht hinreichend geklärt. Um möglichst viele Verifikationstools zu verbessern, ist es unser Ziel, schnellere Algorithmen für diese zentralen Graphprobleme zu entwickeln. Wir werden uns dabei auf die folgenden modernen algorithmischen Techniken konzentrieren: 1. Techniken von dynamischen Graphalgorithmen: Viele Algorithmen, die in Verifikationstools zum Einsatz kommen, führen die gleiche Berechnung auf verwandten Graphen aus, ohne Zwischenergebnisse in Datenstrukturen abzuspeichern. Dynamische Graphalgorithmen werden genau in dieser Situation eingesetzt, allerdings wurden sie bisher nicht für die Graphprobleme der Verifkationstools entwickelt. Wir wollen basierend auf existierenden Techniken der dynamischen Graphalgorithmen neue Datenstrukturen für die zentralen Graphprobleme der Verifikationstools entwickeln. 2. Randomisierung: Viele Graphprobleme können durch Randomisierung schneller gelöst werden, doch nur wenige Verifikationstools benützen randomisierte Algorithmen. Wir wollen versuchen, durch den Einsatz von Randomisierung, Graphalgorithmen in Verifikationstools zu beschleunigen. Verifikationstools benützen üblicherweise eine Abstraktionsebene, die die Implementierung von Algorithmen mit "symbolischen Schritten" effizient ermöglicht. Wir planen daher auch symbolische Versionen unserer Algorithmen zu entwickeln und sie in einem Prototypen zu implementieren.

Eine der zentralesten Herausforderung in der Informatik ist die Entwicklung korrekter Systeme oder Programme. Subtile Fehler in komplexen Systemen können viele Probleme verursachen. Berühmte Beispiele hierfür sind der Pentium-Chip Fehler oder der Softwarefehler, der zum Absturz der Weltraumrakete Ariane 5 führten. Im Gebiet der computergestützten Verifikation werden automatische Techniken entwickelt, die die Korrektheit von Systemen formal analysieren und bei der Entdeckung von subtilen Fehler helfen. Hierbei wird zunächst ein mathematisches Modell des Systems entwickelt. Üblicherweise sind solche Modelle Erweiterungen von Graphenmodellen. In diesen Modellen werden Systemzustände durch Knoten und Systemübergänge durch Kanten repräsentiert. Pfade im Graphen entsprechen dem Verhalten eines Systems. Das mathematische Model wird dann mit einer Spezifikation, die das gewünschte Verhalten des Systems beschreibt, verglichen. Daher sind automatische Verifikationstechniken nichts anderes als Algorithmen zur Analyse der Eigenschaften von Graphen. Durch die immer größere Komplexität von Software und Hardware steigt auch die Bearbeitungszeit existierender Verifikationstools rasant. Um den Einsatz dieser Verifikationstools weiterhin zu gewährleisten, ist es daher dringend erforderlich schnellere Verifikationstechniken zu entwickeln. Zusätzlich wurden auf anderen Gebieten algorithmische Techniken fuer Probleme auf Graphen stark verbessert. Diese werden aber aktuell noch nicht in der Verifikation eingesetzt. In diesem Projekt haben wir moderne graphalgorithmischen Techniken benützt, um schnellere Algorithmen zur Lösung mehrerer klassischer Probleme in der computergestützten Prüfung zu erhalten. In einigen Fällen ist es uns gelungen seit langem bestehende algorithmischen Barrieren für viele grundlegende Probleme zu durchbrechen. Daneben haben wir symbolische Versionen unserer Algorithmen und Prototyp-Implementierungen entwickelt, um die Einsetzbarkeit unserer Methoden im Robotics-Bereich zu zeigen.