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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationComputational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings
Pages114-127
Number of pages14
EditionPART 3
DOIs
Publication statusPublished - Aug 1 2013
Event13th International Conference on Computational Science and Its Applications, ICCSA 2013 - Ho Chi Minh City, Viet Nam
Duration: Jun 24 2013Jun 27 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
NumberPART 3
Volume7973 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other13th International Conference on Computational Science and Its Applications, ICCSA 2013
CountryViet Nam
CityHo Chi Minh City
Period6/24/136/27/13

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Formalization and model checking of SysML state machine diagrams by CSP#'. Together they form a unique fingerprint.

  • Cite this

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