关键词: 系统建模语言（SysML）, 活动图, 模型验证, Spin, Promela

Abstract: As systems modeling language (SysML) lacks of accurate formal definition and correct verification, it can lead to deadlock, live-lock and other bugs in the model. Formal verification methods can be used to improve correctness of the model. In the reason of that traditional formal methods need complex formula deduction and are not easy to be understood, most verifications can only be used by experts and are very time-consuming. To address the problems of model checking, this paper proposes an automated transition and checking approach for SysML multi-level activity diagram. The activity diagram can be decomposed into sub-diagrams and be transformed to the input model of Spin according to previous constructed model. Then, the sub-diagrams are recombined and verified by Spin. The experiment shows that the approach can effectively split complex activity diagrams in real projects and correctly transform sub-diagrams. This indicates that the approach is helpful for model checking evolution.

Key words: systems modeling language (SysML), activity diagram, model checking, Spin, Promela