Understanding and planning Event-B refinement through primitive rationales

Tsutomu Kobayashi, Fuyuki Ishikawa, Shinichi Honiden

研究成果: Conference contribution

3 被引用数 (Scopus)

抄録

Event-B provides a promising feature of refinement to gradually construct a comprehensive specification of a complex system including various aspects. It has unique difficulties to design complexity mitigation, while obeying Event-B consistency rules, among the potentially large possibilities of refinement plans. However, despite of the difficulties, existing studies on specific examples or high-level and intuitive guidelines are missing clear rationales, as well as principles, guidelines or methods supported by the rationales. In response to this problem, this paper presents a method for refinement planning from an informal/semi-formal specification. By defining primitive rationales, the method can eliminate undesirable plans such as the ones failing to mitigate the complexity. In a case study on a popular example from a book, we derived an enough small number of valid plans only by using the general and essential rationales while explaining the one presented in the book.

本文言語English
ホスト出版物のタイトルAbstract State Machines, Alloy, B, TLA, VDM, and Z - 4th International Conference, ABZ 2014, Proceedings
出版社Springer Verlag
ページ277-283
ページ数7
ISBN(印刷版)9783662436516
DOI
出版ステータスPublished - 2014 1 1
外部発表はい
イベント4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014 - Toulouse, France
継続期間: 2014 6 22014 6 6

出版物シリーズ

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

Other

Other4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, ABZ 2014
国/地域France
CityToulouse
Period14/6/214/6/6

ASJC Scopus subject areas

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

フィンガープリント

「Understanding and planning Event-B refinement through primitive rationales」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル