Validierung für schrittweise Verfeinerung

• Antragsteller: Professor Dr. Michael Leuschel
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme
• Förderung: Förderung seit 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434399180

Trotz ihrer Wirksamkeit und jahrelanger Verfechtung ist der praktische Einsatz formaler Methoden immer noch sehr gering. Ein Grund ist, dass sich die aktuellen Methoden und Werkzeuge auf den Verifikationsprozess (wird die Software richtig entwickelt) konzentriert hat und den Validationsaspekt der Qualitätssicherung (wird die richtige Software entwickelt) im Vergleich dazu vernachlässigt hat.Die Verifikation ist der Kern von Verfeinerungs-basierten Entwicklungsmethoden wie Event-B, wo jeder Verfeinerungsschritt die Eigenschaften des abstrakten Modells beibehalten muss. Die Validation findet oft erst statt, wenn die verfeinerten Modelle detailliert genug für eine Ausführung sind. Fehler in den Anforderungen oder deren Interpretation und Umsetzung werden deshalb viel zu spät im Entwicklungsprozess aufgedeckt.Das IVOIRE Projekt wird es ermöglichen den Validierungsprozess kontinuierlich während der Entwicklung und Verfeinerung durchzuführen. Mit Hilfe von Event-B und Rodin, eine Methodik und eine Entwicklungsumgebung auf dem letzten Stand der Forschung, sollen Fortschritte auf drei Ebenen erzielt werden. Auf der formalen, wissenschaftlichen Ebene wird eine präzise Charakterisierung von Validierung im Rahmen von Verfeinerung entwickelt werden. Auf der Ebene der Methodik wird das klassische lineare Verfeinerungskonzept erweitert, um Validierungsobligationen und deren Prüfung darzustellen. Auf der praktischen Ebene wird die Rodin Werkzeugkette um neue Validationswerkzeuge erweitert und einer besseren Integration existierender Validationswerkzeuge ermöglicht. Anhand von verschiedenen Fallstudien wird der IVOIRE Ansatz mit Hilfe dieser Werkzeuge evaluiert.Das IVOIRE Projekt wird folgende Ergebnisse liefern:- Einen verbesserten formalen Entwicklungsprozess basierend auf einem erweiterten Verfeinerungskonzept mit Unterstützung für Validationsaktivitäten.- Eine verbesserte Event-B Werkzeugkette, mit neuen Werkzeugen um Validierungsobligationen zu prüfen (zum Beispiel mit Animation oder Simulation) und um den gesamten Validierungsprozess zu verwalten.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: Österreich
• Kooperationspartner: Professor Dr. Alexander Egyed; Dr. Atif Mashkoor