Overview

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).