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

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

研究成果: Article

抄録

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.

元の言語English
ジャーナルFormal Aspects of Computing
DOI
出版物ステータスPublished - 2019 1 1

Fingerprint

Event-B
Refactoring
Refinement
Model
Predicate

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science

これを引用

@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

AN - SCOPUS:85061398103

JO - Formal Aspects of Computing

JF - Formal Aspects of Computing

SN - 0934-5043

ER -