CAJ | 학술논문

系统建模语言( Systems Modeling Language,SysML)对复杂系统多视角建模时,容易造成多视图描述语义冲突、矛盾等不一致问题,可以通过形式化验证方法,来提高模型的一致性。然而,受制于传统的形式化检测方法不能做到完全自动化,并且需要繁杂的公式推理,导致多数验证方法仅限少数专家使用并且非常耗时。为了解决SysML时序图与活动图模型之间存在的一致性问题,提出一种自动转换验证框架。首先基于已构建的模型和转换规则,将时序图进行分解转换为活动图,然后分别映射为Spin的输入模型,并对模型的交互一致性执行自动化验证。实验结果表明,该方法可以有效识别和转换时序图,并能准确地向Promela实施映射和验证,为一致性验证的演化提供支持。
계통건모어언( Systems Modeling Language,SysML)대복잡계통다시각건모시,용역조성다시도묘술어의충돌、모순등불일치문제,가이통과형식화험증방법,래제고모형적일치성。연이,수제우전통적형식화검측방법불능주도완전자동화,병차수요번잡적공식추리,도치다수험증방법부한소수전가사용병차비상모시。위료해결SysML시서도여활동도모형지간존재적일치성문제,제출일충자동전환험증광가。수선기우이구건적모형화전환규칙,장시서도진행분해전환위활동도,연후분별영사위Spin적수입모형,병대모형적교호일치성집행자동화험증。실험결과표명,해방법가이유효식별화전환시서도,병능준학지향Promela실시영사화험증,위일치성험증적연화제공지지。
As systems modeling language models multiple views for complex system,it can lead to a variety of inconsistent problem in the model. Formal verification methods can be used to improve consistency of the model. In the reason of that traditional formal methods can’t be complete automation and need complex formula deduction,most verification can only be used by experts and it’s very time-consuming. To address the consistent problems of the SysML sequence diagram and activity diagram,propose an automated transition and checking consistency approach. The sequence diagram can be decomposed and transformed to an activity diagram using the mapping rules. The diagrams are mapped to the input model of Spin. Then,the models are analyzed and verified by Spin. The experimental results show that the approach can correctly transform complex sequence diagrams in real projects and effectively verify consistency of them. This indicates that the approach is helpful for model checking evolution.