Modellbasierte Diagnose für Formale Temporale Beschreibungen

Im globalen Wettbewerb hat sich eine hohe Produktqualität als eine der Möglichkeiten herausgestellt, um mit Mitbewerbern konkurrieren zu können. Die Verwendung einer formalen temporalen Sprache zur Beschreibung des Verhaltens eines Protokolls, einer Komponente, oder eines Gesamtsystems ist ein erster Schritt in Richtung hoher Produkt-qualität und eines effizienten Entwicklungsprozesses: Sie verdeutlicht subtile Fragen, die ansonsten in der Mehrdeutigkeit natürlicher Sprachen versteckt bleiben könnten, und ermöglicht den Einsatz automatischer Werkzeuge. Eine formale Verhaltensbeschreibung ist aber offensichtlich nicht ausreichend. Heutige Forschungsprojekte konzentrieren sich jedoch hauptsächlich auf die Verifikationsphase, in der z.B. die Funktion eines Chips auf Konformität mit der Spezifikation geprüft wird, und nicht auf die Unterstützung bei der Erstellung der Spezifikation selbst. Dies ist insofern verwunderlich, da Industrie-Daten aufzeigen, dass rund 50 Prozent der Produktfehler und etwa 80 Prozent des Überarbeitungsaufwandes auf Fehler in der Spezifikationen zurückzuführen sind. Mit diesem Projekt stellen wir uns der Herausforderung die Spezifikationsentwicklung mit Diagnose-Informationen zu unterstützen. Im Besonderen werden wir folgende drei Fragen untersuchen: Warum ist ein bestimmter Trace ein Gegenbeispiel bzw. ein Zeuge? Wo ist der Fehler in der Spezifikation, wenn eine Verhaltensweise durch die Spezifikation unerwartet (nicht) abgedeckt ist? Wie "erklärt" man komplexe temporale Formeln in attraktiver Weise? Zu diesem Zweck werden wir modellbasierte Diagnose (aus dem Bereich der künstlichen Intelligenz) mit im Bereich der formalen temporalen Sprachen und deren Verifikation bekannten Ideen und Technologien (z.B. model-checking) verschmelzen. Mit modellbasierter Diagnose werden wir den Ursprung von während der Entwicklung auftretenden Problemen diagnostizieren, und somit ein zentrales Problem der formalen Spezifikationsentwicklung ansprechen. Eines unserer generellen Ziele wird es sein, dem Benutzer Informationen zu bieten, die direkt auf die Spezifikation bezogen sind und nicht etwa auf einen abgeleiteten Automaten. Für unser Projekt werden wir die Linear Temporal Logic (LTL) und Erweiterungen aus neueren Sprachen wie der Property Specification Language (PSL) betrachten. Obwohl beide Sprachen aus dem Bereich des Software- /Hardwaredesigns stammen, wurde LTL zum Beispiel auch im Bereich der Wissensbasis-Wartung eingesetzt, weswegen wir eine interdisziplinär adaptierbare und attraktive Lösung anbieten werden. Mit unserer Fokusierung auf die diagnostische Unterstützung bei der Entwicklung, Wartung, und Nutzung formaler temporaler Beschreibungen, und der Erhöhung deren Qualität, erwarten wir der Nutzung selbiger in Forschung und Industrie Vorschub leisten zu können. Weiters erwarten wir durch die Integration von Ideen und Technologien verschiedener Forschungsbereiche neue Impulse für weitere Forschungsprojekte generieren zu können.

Für jede(n) von uns haben Missverständnisse in der Kommunikation bereits zu unerwarteten Problemen geführt. Im heutigen Entwurfsprozess unterstützt uns die Verwendung formaler Beschreibungssprachen entsprechende Probleme zu vermeiden und erlaubt uns einzelne Schritte oder das finale Produkt über die Konformität mit einer Spezifikation zu verifizieren. In unserer Forschung widmeten wir uns der Frage Was aber, wenn eine Spezifikation die Überlegungen des Verfassers nicht genau abbildet oder aus anderen Gründen fehlerhaft ist? Wie kann ich den Fehler in der Spezifikation aufgrund von Fehlverhalten identifizieren? Unser Fokus lag dabei auf funktionalen temporalen Verhaltensbeschreibungen, welche, z.B., das zeitliche Verhalten eines Programms oder von Hardware in Bezug auf entsprechende Eingaben oder Eingangssignale beschreiben. Für Amir Pnuelis Temporale Logik für Programme (LTL) die auch für digitale Hardware eingesetzt wird, haben wir gezeigt wie entsprechende Diagnosen über das Formulieren und Lösen spezieller Erfüllbarkeitsprobleme effizient berechnet werden können. Unsere Diagnosen zeigen der Entwicklerin jene Teile (und deren Kombinationen) der Spezifikation die für das unerwartete Verhalten verantwortlich sein können. Über einen erweiterten komplexeren Ansatz können wir unter Beachtung entwickelter Fehlermodelle auch entsprechende Lösungen bzw. Reparaturen berechnen. Ausgehend von unserer Forschung im Kontext von LTL haben wir auch Erweiterungen für komplexere oder komplementäre Formate wie Kontrollflussgraphen für Softwareprogramme (welche von service-orientierten Architekturen abgeleitet wurden) oder Wissensbasen von Robotern untersucht und entwickelt.Die Grundlagen und Konzepte von Diagnose-Berechnungen sind eng mit Überlegungen wie man Spezifikationen erklären oder auch testen könnte verwandt, insbesonders im Kontext der Erforschung welches Verhalten von einer Spezifikation erlaubt (oder spezifiziert) ist und welches nicht. Insofern haben wir uns ebenfalls mit der Identifizierung von charakteristischen Verhaltenssets beschäftigt und dieses Wissen zur Berechnung entsprechender Testsets verwendet, die es uns mit einer hohen Wahrscheinlichkeit erlauben Spezifikationsfehler über entsprechend ausgelöstes Fehlverhalten (mit anschließender Diagnose) aufzudecken. Ein besonderes Augenmerk lag auf der Optimierung unserer Diagnosealgorithmen, sowohl im Kontext der Spezifikationsdiagnose als auch der Diagnosetheorie an sich. So konnten wir diesbezüglich einerseits strukturelle Eigenschaften einer Spezifikation ausnützen, aber auch bekannte Diagnosealgorithmen und deren Bestandteile in theoretischen Aspekten verbessern. Eine entsprechende Bibliothek mit Implementierungen ist frei verfügbar.