Consistency-preserving refactoring of refinement structures in Event-B models

Tsutomu Kobayashi*, Fuyuki Ishikawa, Shinichi Honiden

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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.

Original languageEnglish
Pages (from-to)287-320
Number of pages34
JournalFormal Aspects of Computing
Issue number3
Publication statusPublished - 2019 Jun 1


  • Abstraction
  • Action systems
  • Event-B
  • Interpolation
  • Refactoring
  • Refinement

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science


Dive into the research topics of 'Consistency-preserving refactoring of refinement structures in Event-B models'. Together they form a unique fingerprint.

Cite this