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. © 2013 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Ando, T., Yatsu, H., Kong, W., Hisazumi, K., & Fukuda, A. (2013). Formalization and model checking of SysML state machine diagrams by CSP#. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7973 LNCS, pp. 114–127). https://doi.org/10.1007/978-3-642-39646-5_9
Mendeley helps you to discover research relevant for your work.