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

Keywords

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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Refactoring refinement structure of event-B machines'. Together they form a unique fingerprint.

  • 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