IVOIRE

T rotz ihrer Wirksamkeit und jahrelanger Ve r fe cht ung i s t d e r p r ak ti sc he E i n s at z formaler Methoden immer noch sehr gering. Ein Grund ist, dass sich d i e a k tu el len Methoden und Werkzeuge auf den Verifikationsprozess (wird d i e S o f twa re r i c h ti g entwickelt) konzentriert hat und den Validationsaspekt der Qualitätssicherung ( wi r d die richtige Software entwickelt) im Vergleich dazu vernachlässigt hat. Die Verifikation ist der Kern von Verfeinerungs-basierte n E n t wi ck l ungs met hod en wie Event-B, wo jeder Verfeinerungsschritt die Eigenschaften des abstrakten Modells beibehalten muss. Die Validation findet oft erst statt, wenn die verfeinerte n Modelle detailliert genug für eine Ausführung sind. F eh le r i n d e n A n f o rder unge n oder deren Interpretation und Umsetzung werden deshalb viel zu spät im Entwicklungsprozess aufgedeckt. Das IVOIRE Projekt wird es ermöglichen den Vali di er ungs pro zes s k o n ti nu ier li c h während der Entwicklung und Verfeinerung durchzuführen. Mi t Hi l f e v o n E v e nt -B und Rodin, eine Methodik und eine Entwicklungsumgebung auf dem l e t zt en S t a nd der F orschung, sollen F ortschritte auf drei Ebenen erzielt werden . Auf der formalen, wissenschaftlichen Ebene wird eine präzise Charakterisierung v o n V a l id ie rung i m Rahmen von Verfeinerung entwickelt werden. Auf der Ebene der Methodik wird d a s klassische lineare Verfeinerungskonzept erweitert, um V a l i di eru ngs obl ig ati on en und deren Prüfung darzustellen. Auf der praktischen Ebene wird die Rodin Werkzeugkette um neue Validationswerkzeuge erweitert und einer besseren Integration existier ender Valida tionswerkzeuge ermöglicht. Anhand von verschiedenen F allstudien wird der IVOIRE Ansatz mit Hilfe dieser Werkzeuge evaluiert. Das IVOIRE Projekt wird folgende Ergebnisse liefern: - Einen verbesserten formalen Entwicklungsprozess basierend auf einem erweiterten VerfeinerungskonzeptmitUnterstützungfü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.

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.