CAJ | 학술논문

系统建模语言（systems modeling language，SysML）缺乏精确的形式化分析和验证手段，造成模型存在死锁、活锁等诸多问题，可以通过形式化验证方法来提高模型的正确性。然而，受制于传统的形式化方法需要复杂的公式推理，并且不易理解等方面局限性，大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题，提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型，将多层次活动图分解转换为Spin的输入模型，并对相关子图进行重组和验证。实验表明，该方法可以有效识别多层次活动图，并准确实施转换，为模型验证的演化提供支持。
계통건모어언（systems modeling language，SysML）결핍정학적형식화분석화험증수단，조성모형존재사쇄、활쇄등제다문제，가이통과형식화험증방법래제고모형적정학성。연이，수제우전통적형식화방법수요복잡적공식추리，병차불역리해등방면국한성，대다수험증부한전가사용병차흔모시。위료극복SysML모형중존재적문제，제출료일충침대SysML다층차활동도적분석험증광가。타가이근거이구건적모형，장다층차활동도분해전환위Spin적수입모형，병대상관자도진행중조화험증。실험표명，해방법가이유효식별다층차활동도，병준학실시전환，위모형험증적연화제공지지。
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 cor-rectness 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.