FWF - MoDiaForTeD - 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.