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

摘要： 系统建模语言（systems modeling language，SysML）缺乏精确的形式化分析和验证手段，造成模型存在死锁、活锁等诸多问题，可以通过形式化验证方法来提高模型的正确性。然而，受制于传统的形式化方法需要复杂的公式推理，并且不易理解等方面局限性，大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题，提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型，将多层次活动图分解转换为Spin的输入模型，并对相关子图进行重组和验证。实验表明，该方法可以有效识别多层次活动图，并准确实施转换，为模型验证的演化提供支持。

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