TY - GEN
T1 - Formalization and model checking of SysML state machine diagrams by CSP#
AU - Ando, Takahiro
AU - Yatsu, Hirokazu
AU - Kong, Weiqiang
AU - Hisazumi, Kenji
AU - Fukuda, Akira
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84880753262&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84880753262&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39646-5_9
DO - 10.1007/978-3-642-39646-5_9
M3 - Conference contribution
AN - SCOPUS:84880753262
SN - 9783642396458
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 114
EP - 127
BT - Computational Science and Its Applications, ICCSA 2013 - 13th International Conference, Proceedings
T2 - 13th International Conference on Computational Science and Its Applications, ICCSA 2013
Y2 - 24 June 2013 through 27 June 2013
ER -