Logo der Universität Wien

Modern Graph Algorithmic Techniques in Formal Verification

Table of content
Grafik

Further details
Type
R&D projects, public funding
Duration
2011 - 2015
Executive
Research Group Theory and Applications of Algorithms
Abstract

In Kooperation mit Krishnendu Chatterjee / IST Austria

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 zentrale Graphprobleme zu entwickeln. Wir werden uns dabei auf die folgenden modernen algorithmischen Techniken konzentrieren:

1. Techniken von dynamische 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 wer-den genau in dieser Situation eingesetzt, allerdings wurden sie bisher nicht für die Graphprobleme der Verifkationstools enwickelt. 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.

Grafik Top
Associates
  • Institute of Science and Technology Austria
  • Krishnendu Chatterjee of IST
Grafik Top

Theory and Applications of Algorithms

Faculty of Computer Science
University of Vienna
Währinger Straße 29
A-1090 Vienna

F +43-1-4277-9 783

Universität Wien | Universitätsring 1 | 1010 Wien | T +43-1-4277-0