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

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

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

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

元の言語英語
ホスト出版物のタイトルComputational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings
ページ114-127
ページ数14
エディションPART 3
DOI
出版物ステータス出版済み - 8 1 2013
イベント13th International Conference on Computational Science and Its Applications, ICCSA 2013 - Ho Chi Minh City, ベトナム
継続期間: 6 24 20136 27 2013

出版物シリーズ

名前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

その他

その他13th International Conference on Computational Science and Its Applications, ICCSA 2013
ベトナム
Ho Chi Minh City
期間6/24/136/27/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

フィンガープリント Formalization and model checking of SysML state machine diagrams by CSP#' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Ando, T., Yatsu, H., Kong, W., Hisazumi, K., & Fukuda, A. (2013). Formalization and model checking of SysML state machine diagrams by CSP#. : Computational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings (PART 3 版, pp. 114-127). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 巻数 7973 LNCS, 番号 PART 3). https://doi.org/10.1007/978-3-642-39646-5_9