Integrationstest kom... Forschungsprojekte Versionskontrolle f&...

Verifikation komponentenbasierter Softwaresysteme unter Einbeziehung bewiesener Komponenteneigenschaften


Die sehr hohe Komplexität heutiger Softwaresysteme führt dazu, dass ihre vollständige formale Verifikation kaum zu bewältigen ist. Für sicherheitskritische Systeme ist es allerdings nötig, zumindest einige für die Anwendung relevante Eigenschaften nachweisen zu können.

Softwarekomponenten sind in sich abgeschlossene Softwarebausteine mit einer definierten Schnittstelle. Solche Komponenten können zu einem Gesamtsystem integriert werden. Der Vorteil dieses Ansatzes liegt darin, dass die Komponenten wiederverwendet werden können; eventuell können Komponenten von externen Anbietern hinzugekauft werden. Die Komplexität komponentenbasierter Systeme ist, sowohl durch die Wiederverwendung bewährter Komponenten als auch durch die höhere Verständlichkeit dank der Bausteinzerlegung, leichter zu bewältigen.

Dieser komponentenbasierte Ansatz bietet darüber hinaus auch die Möglichkeit, den Verifikationsaufwand zu verringern. Dazu müssen Komponenteneigenschaften, die anhand der Komponenten überprüft wurden, dokumentiert worden sein. Mittels einer Beschreibung des Systems sollen - von den Komponenteneigenschaften ausgehend - die Systemeigenschaften abgeleitet werden.

Für erwünschte, aber noch nicht ableitbare Systemeigenschaften sollen zusätzliche Komponenteneigenschaften ermittelt werden, aus denen sich erstere herleiten lassen. Mittels Wrappers sollen anschließend die erforderlichen Komponenteneigenschaften erzwungen werden.

Das Projekt beschäftigte sich zunächst mit einer Untersuchung bestehender Komponenten- und Systembeschreibungssprachen. Zu diesem Zwecke wurden mehrere Architekturbeschreibungssprachen (engl. Architectural Description Language, ADL) untersucht und vergleichend bewertend. Dabei wurde ermittelt, in wieweit es diese Sprachen ermöglichen, Aktoren und Sensoren, die durch Komponenten angesteuert werden sowie die Interaktionen zwischen diesen Aktoren und Sensoren zu beschreiben. Insbesondere wurde dabei ermittelt, welche Sprachen eine systemunabhängige Komponentenbeschreibung erlauben.

Ein formales Modell zur Beschreibung des Komponentenverhaltens wurde entwickelt, welches durch eine einfache Transformation auf eine Kripke-Struktur abgebildet werden kann. Dies ergibt eine formale Basis mit Schlussregeln zur Herleitung von Systemeigenschaften aus Komponenteneigenschaften.

Darauf aufbauend wurde untersucht, inwieweit mittels Model-Checker die Einhaltung relativer Zeitanforderungen überprüft werden kann. Dazu gehören beispielsweise Anforderungen an die Konsistenz von Dienstaufrufen und Komponentenzuständen sowie Anforderungen bezüglich der Reihenfolge vorgegebener Dienstaufrufe. Zu diesem Zwecke wurde ein Verfahren entwickelt, das zu einer vorgegebenen relativen Zeitanforderung eine entsprechende Menge von Aussagen in der Computation Tree Logic (CTL) ermittelt, welche anschließend einzeln auf Gültigkeit überprüft werden. Auf diese Weise erhält man bereits während der Komponentenintegration allgemeingültige Aussagen darüber, unter welchen spezifischen Bedingungen die jeweils betrachteten, relativen Zeitanforderungen verletzt werden.

Teilprojekt A: "Bewertung und Vergleich von Verfahren zur Analyse der Aussagekraft von Model-Checking-Nachweisen"

Im Rahmen dieses Teilprojektes wurden mehrere Verfahren zur Analyse der Aussagekraft von Model-Checking-Nachweisen (u. a. Vacuity Detection, Model Checking Coverage, Witness Generation) untersucht. Ein Vergleich der ermittelten Verfahren, insbesondere in Hinblick auf die zugelassenen temporalen Logiken und auf die Aussagekraft der gelieferten Information, u. a. für eine eventuelle Fehlersuche, wurde durchgeführt. Um die Anwendung der untersuchten Verfahren zu erleichtern, wurde ein Werkzeug implementiert, das möglichst viele der identifizierten Verfahren mit Hilfe des Model Checkers NuSMV realisiert und die Ergebnisse weit möglichst visualisiert.

Ausblick: Ein weiterer Schritt in diesem Forschungsprojekt besteht darin, aus den Eigenschaften der Komponenten auf die Eigenschaften des Gesamtsystems schließen zu können. Für Systemeigenschaften, die sich aus den vorgegebenen Komponenteneigenschaften nicht herleiten lassen, ist ein Verfahren anzustreben, welches zusätzliche Komponenteneigenschaften herzuleiten erlaubt, die einen Inferenzschluss auf die Gültigkeit der nachzuweisenden Systemeigenschaften ermöglichen.