Construction of abstract state graphs for understanding event-B models

Daichi Morita, Fuyuki Ishikawa, Shinichi Honiden

研究成果: Conference contribution

抄録

Event-B is a formal method that supports correctness by construction in system modeling using stepwise refinement. However, it is difficult to understand the rigorous behaviors of models from Event-B specifications, such as the reachable state space or the possible sequences of events. This is because the Event-B model is described in a style that lists events that have concurrently been enabled depending on their guard conditions. This paper proposes a method that helps in understanding the rigorous behaviors of an Event-B model by creating an abstract state graph. The core of our method involves dividing the concrete state space by using the guard conditions of individual events to extract states that are essential to enable possible transitions to be understood. Moreover, we further divided the state space by using the guard conditions of events in the models before refinement to support understanding of changes in behaviors between the models before and after refinement. Our unique approach facilitated finding of invariants that were not specified but held, which were useful for validation.

本文言語English
ホスト出版物のタイトルDependable Software Engineering
ホスト出版物のサブタイトルTheories, Tools, and Applications - 3rd International Symposium, SETTA 2017, Proceedings
編集者Ji Wang, Kim Guldstrand Larsen, Oleg Sokolsky
出版社Springer Verlag
ページ250-265
ページ数16
ISBN(印刷版)9783319694825
DOI
出版ステータスPublished - 2017
外部発表はい
イベント3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017 - Changsha, China
継続期間: 2017 10 232017 10 25

出版物シリーズ

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

Other

Other3rd International Symposium on Dependable Software Engineering: Theories, Tools and Applications, SETTA 2017
国/地域China
CityChangsha
Period17/10/2317/10/25

ASJC Scopus subject areas

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

フィンガープリント

「Construction of abstract state graphs for understanding event-B models」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル