Formalization and model checking of SysML state machine diagrams by CSP#

Takahiro Ando, Hirokazu Yatsu, Weiqiang Kong, Kenji Hisazumi, Akira Fukuda

研究成果: Conference contribution

7 被引用数 (Scopus)

抄録

SysML state machine diagrams are used to describe the behavior of blocks in the system under consideration. The work in [1] proposed a formalization of SysML state machine diagrams in which the diagrams were translated into CSP# processes that could be verified by the state-of-the-art model checker PAT. In this paper, we make several modifications and add new rules to the translation described in that work. First, we modify three translation rules, which we think are inappropriately defined according to the SysML definition of state machine diagrams. Next, we add new translation rules for two components of the diagrams - junction and choice pseudostates - which have not been dealt with previously. As the contribution of this work, we can achieve more reasonable verification results for more general SysML state machine diagrams.

本文言語English
ホスト出版物のタイトルComputational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings
ページ114-127
ページ数14
PART 3
DOI
出版ステータスPublished - 2013
外部発表はい
イベント13th International Conference on Computational Science and Its Applications, ICCSA 2013 - Ho Chi Minh City, Viet Nam
継続期間: 2013 6 242013 6 27

出版物シリーズ

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

Conference

Conference13th International Conference on Computational Science and Its Applications, ICCSA 2013
国/地域Viet Nam
CityHo Chi Minh City
Period13/6/2413/6/27

ASJC Scopus subject areas

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

フィンガープリント

「Formalization and model checking of SysML state machine diagrams by CSP#」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル