Integration of Validation into Refinement-based Development (IVOIRE)

将验证集成到基于细化的开发中 (IVOIRE)

• 批准号: 434399180
• 负责人: Professor Dr. Michael Leuschel
• 金额: --
• 依托单位: Institut für Software Systems Engineering (ISSE)
• 依托单位国家: 德国
• 项目类别: Research Grants
• 资助国家: 德国
• 项目状态: 未结题
• 来源: https://gepris.dfg.de/gepris/projekt/434399180?language=en
• 关键词: Integration; Validation; into; Refinement; based

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

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