Consistency-Preserving Refactoring of Refinement Structures in Event-B Models
Consistency-Preserving Refactoring of Refinement Structures in Event-B Models
复制标题
事件 B 模型中细化结构的一致性保持重构
DOI：
10.1007/s00165-019-00478-z
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Shinichi Honiden
中科院分区：
文献类型：
--
作者：
Tsutomu Kobayashi;Fuyuki Ishikawa;Shinichi Honiden
事件B一直吸引着人们的兴趣，因为它支持一种灵活的细化机制，通过考虑模型的多个抽象层，降低了构建和验证复杂目标系统模型的复杂性。虽然大多数以前的研究事件B的重点是模型的构建，所构建的模型需要维护。此外，现有模型的一部分经常被重用以构建其他模型。本文介绍了一种提高现有Event-B模型可维护性和可重用性的方法。它通过构建与原始模型中使用的变量集不同的变量集来自动重建现有模型的细化结构，同时保持在原始模型中检查的重复性。该方法通过从现有模型中提取某些谓词并从现有模型的一致性条件中导出额外的谓词来自动将每个细化步骤分解为多个步骤，以创建与原始模型一致的新模型。该方法将细化步骤的分解与细化步骤的组合相结合，根据重构后模型的细化步骤中需要考虑的给定变量集自动重构细化步骤。实例分析结果表明，该方法能够有效地利用Event-B的细化机制。
Event-B has been attracting much interest because it supports a flexible refinement mechanism that reduces the complexity of constructing and verifying models of complicated target systems by taking into account multiple abstraction layers of the models. Although most previous studies on Event-B focused on model construction, the constructed models need to be maintained. Moreover, parts of existing models are often reused to construct other models. In this paper, a method is introduced that improves the maintainability and reusability of existing Event-B models. It automatically reconstructs the refinement structure of existing models by constructing models about different sets of variables than that used in the original models, while maintaining the consistencies checked in the original models. The method automatically decomposes each refinement step into multiple steps by taking certain predicates from existing models and deriving additional predicates from the consistency conditions of existing models to create new models consistent with the original ones. By combining the decomposing of refinement steps with the composing of refinement steps, this method automatically restructures a refinement step in accordance with given sets of variables to be taken into account in refinement steps of the refactored models. The results of case studies in which large refinement steps in existing models were decomposed and existing models were restructured to extract reusable parts for constructing other models demonstrated that the proposed method facilitates effective use of the refinement mechanism of Event-B.