Refactoring refinement structure of event-B machines

Tsutomu Kobayashi*, Fuyuki Ishikawa, Shinichi Honiden

*この研究の対応する著者

研究成果: Conference contribution

7 被引用数 (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.

本文言語English
ホスト出版物のタイトルFM 2016
ホスト出版物のサブタイトルFormal Methods - 21st International Symposium, Proceedings
編集者Constance Heitmeyer, Anna Philippou, Stefania Gnesi, John Fitzgerald
出版社Springer Verlag
ページ444-459
ページ数16
ISBN(印刷版)9783319489889
DOI
出版ステータスPublished - 2016
外部発表はい
イベント21st International Symposium on Formal Methods, FM 2016 - Limassol, Cyprus
継続期間: 2016 11 92016 11 11

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9995 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

Other

Other21st International Symposium on Formal Methods, FM 2016
国/地域Cyprus
CityLimassol
Period16/11/916/11/11

ASJC Scopus subject areas

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「Refactoring refinement structure of event-B machines」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル