TY - GEN
T1 - Refactoring refinement structure of event-B machines
AU - Kobayashi, Tsutomu
AU - Ishikawa, Fuyuki
AU - Honiden, Shinichi
N1 - Funding Information:
This work is partially supported by JSPS KAKENHI Grant Number 26700005.
Publisher Copyright:
© Springer International Publishing AG 2016.
PY - 2016
Y1 - 2016
N2 - Refinement in formal specifications has received significant attention as a method to gradually construct a rigorous model. Although refactoring methods for formal specifications have been proposed, there are no methods for refactoring of refinement structures in formal specifications. In this paper, we describe a method to restructure refinements in specifications of Event-B, a formal specification method with supports for refinement. The core of our method is decomposition of refinements. Namely, when an abstract Event-B machine A, a concrete machine C refining A, and a slicing strategy are provided, our method constructs a consistent intermediate machine B, which refines A and is refined by C. We show effectiveness of our methods through two case studies on representative usages of our method: decomposition of large-scale refinements and extraction of reusable parts of specifications.
AB - Refinement in formal specifications has received significant attention as a method to gradually construct a rigorous model. Although refactoring methods for formal specifications have been proposed, there are no methods for refactoring of refinement structures in formal specifications. In this paper, we describe a method to restructure refinements in specifications of Event-B, a formal specification method with supports for refinement. The core of our method is decomposition of refinements. Namely, when an abstract Event-B machine A, a concrete machine C refining A, and a slicing strategy are provided, our method constructs a consistent intermediate machine B, which refines A and is refined by C. We show effectiveness of our methods through two case studies on representative usages of our method: decomposition of large-scale refinements and extraction of reusable parts of specifications.
KW - Abstraction
KW - Event-B
KW - Interpolation
KW - Refactoring
KW - Refinement
UR - http://www.scopus.com/inward/record.url?scp=84996598332&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84996598332&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-48989-6_27
DO - 10.1007/978-3-319-48989-6_27
M3 - Conference contribution
AN - SCOPUS:84996598332
SN - 9783319489889
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 444
EP - 459
BT - FM 2016
A2 - Heitmeyer, Constance
A2 - Philippou, Anna
A2 - Gnesi, Stefania
A2 - Fitzgerald, John
PB - Springer Verlag
T2 - 21st International Symposium on Formal Methods, FM 2016
Y2 - 9 November 2016 through 11 November 2016
ER -