Forschungsaktivitäten
Projekt: Software-Verifikation (Software Model-Checking)
Je mehr unsere Gesellschaft und unser persönliches Leben von computerbasierten Geräten abhängt,
desto wichtiger ist die korrekte Funktionstüchtigkeit der Computer-Programme,
die in solchen Geräten laufen:
Vom korrekten Funktionieren unserer Handys und Telefonanlagen hängt es ab,
ob wir im Notfall effizient Hilfe rufen können;
von der Zuverlässigkeit des Bremssystems unseres Autos hängt es ab,
ob wir ggf. einen Unfall vermeiden können.
In beiden Fällen sind die wesentlichen funktionalen Bausteine in Software realisiert.
Der Lehrstuhl ist einer der drei führenden Entwickler von Verifikationssoftware für C-Programme.
Das Werkzeug CPAchecker bekommt als Eingabe ein C-Programm und eine Spezifikation und
untersucht mit erschöpfender Genauigkeit, ob die Spezifikation im gegebenen Programm verletzt werden kann,
das heißt, ob eine Fehlfunktion möglich ist.
Das Projekt leistet wichtige Beiträge zur Steigerung von Effizienz und Effektivität moderner Verifikationstechnologien.
Das Projekt wird in Zusammenarbeit mit der Simon Fraser University in Kanada durchgeführt.
Projekt: Strukturanalyse und Verstehen großer Softwaresysteme
Ein wichtiges Kriterium der Qualität von Software ist der innere Aufbau (Struktur) des gegebenen Softwaresystems.
Wohlstrukturiertheit ist Voraussetzung für erfolgreiche
Wartungs-, Erweiterungs- und Reparaturarbeiten an großen Softwaresystemen.
Software-Clustering ist eine wichtige Methode, um in einem Reverse-Engineering-Prozess
abstrakte Strukturbeschreibungen für Softwaresysteme zu erzeugen.
Das Programm CCVisu, ein vom Lehrstuhl geleitetes Open-Source-Projekt
zur automatischen Generierung von Struktur-Visualisierungen, ist ein beliebtes
und vielfach angewendetes Werkzeug zum Graph-Clustering.
Dabei werden die Softwareartefakte so in Teilsysteme aufgeteilt,
dass diese möglichst unabhängig voneinander verstanden und verändert werden können.
Dieses Projekt leistet auch wichtige Beiträge zur Entwicklung von Maßen zur
quantitativen Erfassung von Strukturiertheit und Verständlichkeit von Softwaresystemen.
Projekt: Komponentenbasierter Software-Entwurf
Ein Ziel moderner Software-Architekturen ist es, die Teilsysteme möglichst unabhängig voneinander zu gestalten.
Das heißt, ein Teilsystem soll vom anderen gerade so viel wissen,
wie zur Nutzung der angebotenen Dienste erforderlich ist, aber keinesfalls mehr.
Dieses Ziel wird nahezu vollständig erreicht von so genannten Web-Service-Architekturen,
bei denen die einzelnen Teilsysteme auf verschiedenen Rechnern in möglicherweise mehreren Ländern
laufen und nicht mittels Funktionsaufrufe kommunizieren, sondern über Text-Nachrichten.
Die Implementierungsdetails der Teilsysteme sind nicht bekannt, sondern nur deren Verhaltensbeschreibung.
Um solche Systeme erfolgreich zu verifizieren, muss das Verhalten formal modelliert werden.
Am Lehrstuhl werden Modellierungssprachen zur Beschreibung komponentenbasierter Systeme und
deren Eigenschaften entwickelt und erprobt.
Momentan wird an der Implementierung eines Werkzeugs zur automatischen Verifikation, das heißt zur Berechnung
eines Korrektheitszertifikats, gearbeitet.
