Integration of Validation into Refinement-based Development (IVOIRE)

尽管它们通过构建和数十年的倡导有效地生成正确的软件，但严格方法的份额在当代软件开发中仍然非常低。造成这种情况的主要原因之一是，当前严格的方法及其支持环境主要集中在质量保证过程的一半：验证（我们构建软件正确吗？）另一半，验证（我们构建了正确的软件吗？），得到的关注要少得多。验证是基于细化的严格方法的核心，例如Event-B，其中每个后续的细化步骤必须保留其抽象模型的所有属性。验证通常被推迟到开发的最后阶段，当模型足够详细可以执行时。因此，发现需求或需求解释中的错误就太晚了。科特迪瓦项目将通过逐步改进使正式模型在开发过程中不断得到验证。使用Event-B和Rodin，一种最先进的严格方法及其支持环境，科特迪瓦公司打算在三个层次上提供与正式规范验证相关的问题的答案。在科学层面上，它提出了验证和细化之间关系的形式化表征。在方法层面上，它提出了对线性细化的传统概念的扩展，其中还包括称为“验证义务”的验证活动。在实践层面，它提出了新的验证工具的原型，并将现有工具更好地集成到规范编写过程中，规范编写过程可以常规地用于验证模型。科特迪瓦提供的答案将通过两个医学案例研究加以验证。IVOIRE项目最终将产生：•一个基于细化框架扩展的增强的正式开发过程，包括一个全面的验证过程，以及•一个丰富的Event-B工具集，用于执行验证义务（例如，通过动画或模拟）和管理整个验证过程（例如，场景管理器）。

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