Integration of Validation into Refinement-based Development (IVOIRE)

• Applicant: Professor Dr. Michael Leuschel
• Subject Area: Software Engineering and Programming Languages ; Security and Dependability, Operating-, Communication- and Distributed Systems
• Term: from 2020 to 2025
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 434399180

• Final Report Year: 2025

Final Report Abstract

Formal methods and their support environments primarily focus on one half of the quality-assurance process: verification (do we build software right?). The other half, validation (do we build right software?), has been given less attention. While verification is the core of refinementbased formal methods, where each new refinement step must preserve all properties of its abstract model, validation is usually postponed until the latest stages of the development, when models can be automatically executed. Thus, mistakes in requirements or their interpretation are caught too late: usually at the end of the development process. In the IVOIRE project, we introduced a systematic approach for the validation of formal models, based on the novel concept of validation obligations (VOs), that ensures that a formal model correctly captures stakeholders’ requirements, helps discover missing requirements, and enables stakeholders to evaluate whether and how their requirements have evolved over time. Our research is primarily based on the formal methods B and Event-B and their ecosystem (environment, tools, etc.), although the concept of VOs is not limited to these specific formal methods. Key contributions of the IVOIRE project include the formalization of VOs, the validation-driven development (VDD) approach, a nonlinear refinement concept for B and Event-B, analysis of the effects of refinement on traces, implementation of the VO manager tool, improvements and extensions of existing verification/validation tools (namely ProB and Rodin), and case studies evaluating the effectiveness of the developed techniques and tools.

Publications

• 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