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

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

Research output: Contribution to journalArticle

Abstract

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
JournalFormal Aspects of Computing
DOIs
Publication statusPublished - 2019 Jan 1

Fingerprint

Event-B
Refactoring
Refinement
Model
Predicate

Keywords

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

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science

Cite this

Consistency-preserving refactoring of refinement structures in Event-B models. / Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi.

In: Formal Aspects of Computing, 01.01.2019.

Research output: Contribution to journalArticle

@article{027bdaad942346559bdea68d3c508902,
title = "Consistency-preserving refactoring of refinement structures in Event-B models",
abstract = "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.",
keywords = "Abstraction, Action systems, Event-B, Interpolation, Refactoring, Refinement",
author = "Tsutomu Kobayashi and Fuyuki Ishikawa and Shinichi Honiden",
year = "2019",
month = "1",
day = "1",
doi = "10.1007/s00165-019-00478-z",
language = "English",
journal = "Formal Aspects of Computing",
issn = "0934-5043",
publisher = "Springer London",

}

TY - JOUR

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

AU - Kobayashi, Tsutomu

AU - Ishikawa, Fuyuki

AU - Honiden, Shinichi

PY - 2019/1/1

Y1 - 2019/1/1

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

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

KW - Abstraction

KW - Action systems

KW - Event-B

KW - Interpolation

KW - Refactoring

KW - Refinement

UR - http://www.scopus.com/inward/record.url?scp=85061398103&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061398103&partnerID=8YFLogxK

U2 - 10.1007/s00165-019-00478-z

DO - 10.1007/s00165-019-00478-z

M3 - Article

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

ER -