IVOIRE

Despite their efficacy to generate software correct by construction and decades-long advocacy, the share of rigorous methods is still very low in the contemporary software development. One of the major reasons for this situation is that current rigorous methods and their support environments focus mainly on one half of the quality-assurance process: verification (do we build software right?). The other half, validation (do we build the right software?), has been given much less attention. Verification is at the core of refinement - based rigorous methods, such as Event-B, where each successive refinement step must preserve all properties of its abstract model. Validation is usually postponed until the latest stages of the development, when models are detailed enough to be executed. Mistakes in requirements or their interpretation are thus caught too late. The IVOIRE project will enable continuous validation of formal models during their development by stepwise refinement. Using Event-B and Rodin, a state-of-the-art rigorous method and its support environment, IVOIRE intends to provide answers for issues associated with validation of formal specifications at three levels. At the scientific level, it proposes a formal characterization of the relation between validation and refinement. At the methodological level, it proposes an extension to the conventional notion of linear refinement that also includes validation activities called validation obligations. At the practical level, it proposes prototyping of new validation tools and better integration of existing ones into the specification writing process which can be used routinely to validate models. The answers produced by IVOIRE will be validated through two industrial case studies. The IVOIRE project will ultimately result in: An enhanced formal development process based on the extension of the refinement framework that includes a comprehensive validation process, and An enriched Event-B toolset to perform validation obligations (for example, through animation or simulation) and to manage the overall validation process (for example, scenario managers).

Despite their efficacy in generating software correctly through construction and decades-long advocacy, the share of rigorous methods is still very low in contemporary software development. One of the primary reasons for this situation is that current rigorous methods and their support environments focus mainly on one half of the quality-assurance process: verification (do we build software right?). The other half, validation (do we build the right software?), has been given much less attention. Verification is at the core of refinement-based rigorous methods, such as Event-B, where each successive refinement step must preserve all properties of its abstract model. Validation is usually postponed until the latest stages of development when models are detailed enough to be executed. Mistakes in requirements or their interpretation are thus caught too late. The IVOIRE project enables continuous validation of formal models during their development by stepwise refinement. IVOIRE answers issues associated with validating formal specifications at three levels using Event-B and Rodin, a state-of-the-art rigorous method, and its support environment. At the scientific level, it proposes a formal characterization of the relation between validation and refinement. At the methodological level, it proposes an extension to the conventional notion of linear refinement, including validation activities called "validation obligations." At the practical level, it proposes prototyping new validation tools and better integrating existing ones into the specification writing process, which can be used routinely to validate models. The answers produced by IVOIRE are validated through industrial case studies. The IVOIRE project ultimately results in: An enhanced formal development process based on the extension of the refinement framework that includes a comprehensive validation process and An enriched Event-B toolset to perform validation obligations (for example, through animation or simulation) and to manage the overall validation process (for example, scenario managers).