FWF - MoDiaForTeD - Modellbasierte Diagnose für Formale Temporale Beschreibungen

  • Quaritsch, Thomas, (Teilnehmer (Co-Investigator))
  • Pill, Ingo Hans (Projektleiter (Principal Investigator))

Projekt: Foschungsprojekt

Beschreibung

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.
StatusAbschlussdatum
Tatsächlicher Beginn/ -es Ende1/11/1030/06/15