[1]胡良文,马金晶,孙博. 基于Spin的SysML时序图与活动图一致性检测[J].计算机技术与发展,2015,25(09):31-36.
　HU Liang-wen,MA Jin-jing,SUN Bo. Consistency Check Between SysML Sequence and Activity Diagram Based on Spin[J].,2015,25(09):31-36.
点击复制

 基于Spin的SysML时序图与活动图一致性检测()
分享到：

《计算机技术与发展》[ISSN:1006-6977/CN:61-1281/TN]

卷:
25
期数:
2015年09期
页码:
31-36
栏目:
智能、算法、系统工程
出版日期:
2015-09-10

文章信息/Info

Title:
 Consistency Check Between SysML Sequence and Activity Diagram Based on Spin
文章编号:
1673-629X（2015)09-0031-06
作者:
 胡良文; 马金晶; 孙博
 南京航空航天大学 计算机科学与技术学院
Author(s):
 HU Liang-wen; MA Jin-jing; SUN Bo
关键词:
 ; 系统建模语言; 模型检测; 时序图; 活动图
Keywords:
 ; SysML; model checking; sequence diagram; activity diagram
分类号:
TP311
文献标志码:
A
摘要:
 系统建模语言( Systems Modeling Language,SysML)对复杂系统多视角建模时,容易造成多视图描述语义冲突、矛盾等不一致问题,可以通过形式化验证方法,来提高模型的一致性。然而,受制于传统的形式化检测方法不能做到完全自动化,并且需要繁杂的公式推理,导致多数验证方法仅限少数专家使用并且非常耗时。为了解决SysML时序图与活动图模型之间存在的一致性问题,提出一种自动转换验证框架。首先基于已构建的模型和转换规则,将时序图进行分解转换为活动图,然后分别映射为Spin的输入模型,并对模型的交互一致性执行自动化验证。实验结果表明,该方法可以有效识别和转换时序图,并能准确地向Promela实施映射和验证,为一致性验证的演化提供支持。
Abstract:
 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.

相似文献/References:

[1]赵立军.基于SysML的需求分析研究[J].计算机技术与发展,2011,(12):139.
　ZHAO Li-jun.Research on Requirement Analysis Based on SysML[J].,2011,(09):139.
[2]张志宏,吴庆波,邵立松,等.基于飞腾平台TOE协议栈的设计与实现[J].计算机技术与发展,2014,24(07):1.
　ZHANG Zhi-hong,WU Qing-bo,SHAO Li-song,et al. Design and Implementation of TCP/IP Offload Engine Protocol Stack Based on FT Platform[J].,2014,24(09):1.
[3]梁文快,李毅. 改进的基因表达算法对航班优化排序问题研究[J].计算机技术与发展,2014,24(07):5.
　LIANG Wen-kuai,LI Yi. Research on Optimization of Flight Scheduling Problem Based on Improved Gene Expression Algorithm[J].,2014,24(09):5.
[4]黄静,王枫,谢志新,等. EAST文档管理系统的设计与实现[J].计算机技术与发展,2014,24(07):13.
　HUANG Jing,WANG Feng,XIE Zhi-xin,et al. Design and Implementation of EAST Document Management System[J].,2014,24(09):13.
[5]侯善江[],张代远[][][]. 基于样条权函数神经网络P2P流量识别方法[J].计算机技术与发展,2014,24(07):21.
　HOU Shan-jiang[],ZHANG Dai-yuan[][][]. P2P Traffic Identification Based on Spline Weight Function Neural Network[J].,2014,24(09):21.
[6]李璨,耿国华,李康,等. 一种基于三维模型的文物碎片线图生成方法[J].计算机技术与发展,2014,24(07):25.
　LI Can,GENG Guo-hua,LI Kang,et al. A Method of Obtaining Cultural Debris’ s Line Chart Based on Three-dimensional Model[J].,2014,24(09):25.
[7]翁鹤,皮德常. 混沌RBF神经网络异常检测算法[J].计算机技术与发展,2014,24(07):29.
　WENG He,PI De-chang. Chaotic RBF Neural Network Anomaly Detection Algorithm[J].,2014,24(09):29.
[8]刘茜[],荆晓远[],李文倩[],等. 基于流形学习的正交稀疏保留投影[J].计算机技术与发展,2014,24(07):34.
　LIU Qian[],JING Xiao-yuan[,LI Wen-qian[],et al. Orthogonal Sparsity Preserving Projections Based on Manifold Learning[J].,2014,24(09):34.
[9]尚福华,李想,巩淼. 基于模糊框架-产生式知识表示及推理研究[J].计算机技术与发展,2014,24(07):38.
　SHANG Fu-hua,LI Xiang,GONG Miao. Research on Knowledge Representation and Inference Based on Fuzzy Framework-production[J].,2014,24(09):38.
[10]叶偲,李良福,肖樟树. 一种去除运动目标重影的图像镶嵌方法研究[J].计算机技术与发展,2014,24(07):43.
　YE Si,LI Liang-fu,XIAO Zhang-shu. Research of an Image Mosaic Method for Removing Ghost of Moving Targets[J].,2014,24(09):43.

更新日期/Last Update: 2015-10-16