Refactoring refinement structure of event-B machines

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

Research output: Chapter in Book/Report/Conference proceedingConference contribution

7 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationFM 2016
Subtitle of host publicationFormal Methods - 21st International Symposium, Proceedings
PublisherSpringer-Verlag
Pages444-459
Number of pages16
ISBN (Print)9783319489889
DOIs
Publication statusPublished - 2016 Jan 1
Externally publishedYes
Event21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
Duration: 2016 Nov 92016 Nov 11

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9995 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other21st International Symposium on Formal Methods, FM 2016
CountryCyprus
CityLimassol
Period16/11/916/11/11

Fingerprint

Event-B
Refactoring
Refinement
Formal Specification
Decomposition
Specifications
Refining
Concretes
Specification
Formal specification
Slicing
Decomposition Method
Decompose

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Kobayashi, T., Ishikawa, F., & Honiden, S. (2016). Refactoring refinement structure of event-B machines. In FM 2016: Formal Methods - 21st International Symposium, Proceedings (pp. 444-459). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9995 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-48989-6_27

Refactoring refinement structure of event-B machines. / Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi.

FM 2016: Formal Methods - 21st International Symposium, Proceedings. Springer-Verlag, 2016. p. 444-459 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9995 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kobayashi, T, Ishikawa, F & Honiden, S 2016, Refactoring refinement structure of event-B machines. in FM 2016: Formal Methods - 21st International Symposium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9995 LNCS, Springer-Verlag, pp. 444-459, 21st International Symposium on Formal Methods, FM 2016, Limassol, Cyprus, 16/11/9. https://doi.org/10.1007/978-3-319-48989-6_27
Kobayashi T, Ishikawa F, Honiden S. Refactoring refinement structure of event-B machines. In FM 2016: Formal Methods - 21st International Symposium, Proceedings. Springer-Verlag. 2016. p. 444-459. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-48989-6_27
Kobayashi, Tsutomu ; Ishikawa, Fuyuki ; Honiden, Shinichi. / Refactoring refinement structure of event-B machines. FM 2016: Formal Methods - 21st International Symposium, Proceedings. Springer-Verlag, 2016. pp. 444-459 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f79edfbda9194c6cb1d282d1d9f2b2aa,
title = "Refactoring refinement structure of event-B machines",
abstract = "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.",
keywords = "Abstraction, Event-B, Interpolation, Refactoring, Refinement",
author = "Tsutomu Kobayashi and Fuyuki Ishikawa and Shinichi Honiden",
year = "2016",
month = "1",
day = "1",
doi = "10.1007/978-3-319-48989-6_27",
language = "English",
isbn = "9783319489889",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "444--459",
booktitle = "FM 2016",

}

TY - GEN

T1 - Refactoring refinement structure of event-B machines

AU - Kobayashi, Tsutomu

AU - Ishikawa, Fuyuki

AU - Honiden, Shinichi

PY - 2016/1/1

Y1 - 2016/1/1

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

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

PB - Springer-Verlag

ER -