Refactoring refinement structure of event-B machines

Tsutomu Kobayashi*, Fuyuki Ishikawa, Shinichi Honiden

*Corresponding author for this work

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

7 Citations (Scopus)


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
EditorsConstance Heitmeyer, Anna Philippou, Stefania Gnesi, John Fitzgerald
PublisherSpringer Verlag
Number of pages16
ISBN (Print)9783319489889
Publication statusPublished - 2016
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


Other21st International Symposium on Formal Methods, FM 2016


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


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

Cite this