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 von 2020 bis 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 434399180

• Erstellungsjahr: 2025

Zusammenfassung der Projektergebnisse

Formalen Methoden und die dazugehörigen Werkzeuge konzentrieren sich oft auf den Verifikationsprozess (wird die Software richtig entwickelt?). Der Validierungsaspekt (wird die richtige Software entwickelt?) stand hingegen bisher weniger im Fokus. Die Verifikation ist der Kern von verfeinerungsbasierten Entwicklungsmethoden, wo jeder Verfeinerungsschritt die Eigenschaften des abstrakten Modells beibehalten muss. Die Validierung findet hingegen oft erst in einem späten Entwicklungsschritt statt, wenn die verfeinerten Modelle detailliert genug für eine Ausführung sind. Fehler in den Anforderungen oder deren Interpretation werden deshalb viel zu spät im Entwicklungsprozess aufgedeckt. Das IVOIRE-Projekt hat auf Grundlage des neuartigen Konzepts von Validierungsobligationen (VOs) einen systematischen Ansatz zur Validierung von formalen Modellen eingeführt, welcher sicherstellt, dass ein formales Modell die Anforderungen der Stakeholder korrekt widerspiegelt, bei der Aufspürung von fehlenden Anforderungen hilft, und es den Stakeholdern ermöglicht, einzuschätzen, ob und wie ihre Anforderungen sich im Laufe der Zeit entwickelt haben. Unsere Forschung baut hauptsächlich auf den formalen Methoden B und Event-B sowie deren Ökosystem und Werkzeugen auf, wobei das Konzept von VOs nicht auf diese beiden formalen Methoden beschränkt ist. Zu den Kernbeiträgen des IVOIRE-Projekts gehören die Formalisierung von VOs, der Ansatz der validierungsgetriebenen Entwicklung (VDD), ein Konzept für nichtlineare Verfeinerung, die Analyse der Auswirkungen von Verfeinerung auf Traces, die Implementierung des VO-Manager-Werkzeugs, Verbesserungen und Erweiterungen an vorhandenen Verifikations-/Validierungswerkzeugen (speziell ProB und Rodin), sowie Fallstudien welche die Effektivität der entwickelten Techniken und Werkzeuge auswerten.

Projektbezogene Publikationen (Auswahl)

• Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification. 2021 IEEE/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), 1-5. IEEE.
  Mashkoor, Atif; Leuschel, Michael & Egyed, Alexander
  
• Validation of Formal Models by Timed Probabilistic Simulation. Lecture Notes in Computer Science, 81-96. Springer International Publishing.
  Vu, Fabian; Leuschel, Michael & Mashkoor, Atif
  
• Application of Validation Obligations to Security Concerns. Communications in Computer and Information Science, 337-346. Springer International Publishing.
  Stock, Sebastian; Mashkoor, Atif & Egyed, Alexander
  
• Generating Domain-Specific Interactive Validation Documents. Lecture Notes in Computer Science, 32-49. Springer International Publishing.
  Vu, Fabian; Happe, Christopher & Leuschel, Michael
  
• Model Checking B Models via High-Level Code Generation. Lecture Notes in Computer Science, 334-351. Springer International Publishing.
  Vu, Fabian; Brandt, Dominik & Leuschel, Michael
  
• Trace Refinement in B and Event-B. Lecture Notes in Computer Science, 316-333. Springer International Publishing.
  Stock, Sebastian; Mashkoor, Atif; Leuschel, Michael & Egyed, Alexander
  
• Early and Systematic Validation of Formal Models. Lecture Notes in Computer Science, 255-260. Springer Nature Singapore.
  Stock, Sebastian
  
• Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations. Lecture Notes in Computer Science, 284-302. Springer Nature Switzerland.
  Geleßus, David; Stock, Sebastian; Vu, Fabian; Leuschel, Michael & Mashkoor, Atif
  
• Validation by Abstraction and Refinement. Lecture Notes in Computer Science, 160-178. Springer Nature Switzerland.
  Stock, Sebastian; Vu, Fabian; Geleßus, David; Leuschel, Michael; Mashkoor, Atif & Egyed, Alexander
  
• Validation of Formal Models by Interactive Simulation. Lecture Notes in Computer Science, 59-69. Springer Nature Switzerland.
  Vu, Fabian & Leuschel, Michael
  
• Validation-Driven Development. Lecture Notes in Computer Science, 191-207. Springer Nature Singapore.
  Stock, Sebastian; Mashkoor, Atif & Egyed, Alexander
  
• Early and Systematic Validation of Formal Models. 266 pages. June. Johannes Kepler University Linz.
  Sebastian Stock
  
• Generating interactive documents for domain-specific validation of formal models. International Journal on Software Tools for Technology Transfer, 26(2), 147-168.
  Vu, Fabian; Happe, Christopher & Leuschel, Michael
  
• Trace preservation in B and Event-B refinements. Journal of Logical and Algebraic Methods in Programming, 137, 100943.
  Stock, Sebastian; Mashkoor, Atif; Leuschel, Michael & Egyed, Alexander
  
• Validation of Reinforcement Learning Agents and Safety Shields with ProB. NASA Formal Methods, 279–297.
  Vu, Fabian; Dunkelau, Jannik & Leuschel, Michael
  
• Failure Divergence Refinement for Event-B. Lecture Notes in Computer Science, 85-103. Springer Nature Switzerland.
  Stock, Sebastian; Leuschel, Michael & Mashkoor, Atif
  
• Development and Validation of a Formal Model and Prototype for an Air Traffic Control System. Formal Aspects of Computing, 38(1), 1-37.
  Geleßus, David; Stock, Sebastian; Vu, Fabian; Leuschel, Michael & Mashkoor, Atif