Extracting Traceability between Predicates in Event-B Refinement

Shinnosuke Saruwatari, Fuyuki Ishikawa, Tsutomu Kobayashi, Shinichi Honiden

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

Event-B requires engineers to satisfy proof obligations and inherit all predicates from abstract models while constructing concrete ones. Engineers typically derive predicates from abstract models through transformation with the intention of gradually refining the models. These kinds of intentions for refinement are essential for other engineers to understand the refinements. However, these are implicit and not directly specified in the models. Therefore, it is difficult to understand how each predicate in concrete models is obtained from the predicates in abstract models. This paper proposes an effective method of extracting these relationships. Our approach uses heuristics to avoid exhaustive matching between predicates. It tries to find a set of related predicates by tracing elements, such as variables and constants in predicates, and excluding predicates that use common variables, but differently. Our method facilitates understanding of the intentions of refinements and can be used to help reverse engineering by clarifying the relationships between predicates through refinements.

本文言語English
ホスト出版物のタイトルProceedings - 24th Asia-Pacific Software Engineering Conference, APSEC 2017
編集者Jian Lv, He Zhang, Xiao Liu, Mike Hinchey
出版社IEEE Computer Society
ページ61-70
ページ数10
ISBN(電子版)9781538636817
DOI
出版ステータスPublished - 2018 3 1
外部発表はい
イベント24th Asia-Pacific Software Engineering Conference, APSEC 2017 - Nanjing, Jiangsu, China
継続期間: 2017 12 42017 12 8

出版物シリーズ

名前Proceedings - Asia-Pacific Software Engineering Conference, APSEC
2017-December
ISSN(印刷版)1530-1362

Other

Other24th Asia-Pacific Software Engineering Conference, APSEC 2017
CountryChina
CityNanjing, Jiangsu
Period17/12/417/12/8

ASJC Scopus subject areas

  • Software

フィンガープリント 「Extracting Traceability between Predicates in Event-B Refinement」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル