[1]邓刘梦,葛晓瑜,宛伟健.基于 NuSMV 的 SysML 模型形式化验证[J].计算机技术与发展,2019,29(10):153-156.[doi:10. 3969 / j. issn. 1673-629X. 2019. 10. 030]
　DENG Liu-meng,GE Xiao-yu,WAN Wei-jian.Formal Verification of SysML Model Based on NuSMV[J].,2019,29(10):153-156.[doi:10. 3969 / j. issn. 1673-629X. 2019. 10. 030]
点击复制

基于 NuSMV 的 SysML 模型形式化验证()
分享到：

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

卷:
29
期数:
2019年10期
页码:
153-156
栏目:
智能、算法、系统工程
出版日期:
2019-10-10

文章信息/Info

Title:
Formal Verification of SysML Model Based on NuSMV
文章编号:
1673-629X(2019)10-0153-04
作者:
邓刘梦; 葛晓瑜; 宛伟健
南京航空航天大学 计算机科学与技术学院,江苏 南京 211106
Author(s):
DENG Liu-meng; GE Xiao-yu; WAN Wei-jian
School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China
关键词:
需求工程; 模型转换; 形式化验证; 模型驱动开发
Keywords:
requirement engineering; model transformation; formal verification; model driven development
分类号:
TP311
DOI:
10. 3969 / j. issn. 1673-629X. 2019. 10. 030
摘要:
航空航天道路交通等高安全领域的系统开发需要保证高安全、高可靠,对于该类系统的合理建模以及模型验证则尤为重要。 当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制开发时间和成本,并降低系统出现风险的可能性。 但与此同时,需求与设计模型之间仍然存在着沟壑,设计模型是否很好地满足用户所提出的需求在完成系统设计后仍需验证。 针对系统建模语言缺乏精确形式化语义难以进行模型验证的问题,文中给出一套从 SysML 设计模型到 NuSMV 模型转换的语义规则,实现了一个自动转换程序,将SysML 模型文件转换成 NuSMV 输入文件,进而利用 NuSMV 实现 SysML 模型的验证。 最后通过一个铁路控制系统的案例证明了该方法的有效性。
Abstract:
System development in aerospace road traffic and other high security areas needs to ensure high security and high reliability. It is especially important for the reasonable modeling and model verification of such systems. The model driven development (MDD) method has been widely used in the development of safety-critical systems,which supports the safety analysis and verification of the system at an early stage,effectively controlling development time and cost and reducing the possibility of system risk. At the same time, there is still a gap between the textual requirement and the design model. Whether the design model can well meet the user’s requirements still needs to be verified after the completion of the system design. Addressing the problem of the lack of precise formal semantics for the systems modeling language (SysML),a set of semantic rules for the transformation from SysML design model to NuSMV model is given. An automatic conversion program is implemented to convert the SysML model file into NuSMV input file,and then to verify the SysML model by NuSMV. In the end,we prove the effectiveness of this method through the case of railway control system.

相似文献/References:

[1]王建光 段富.一种UML模型到XML模型的转换方法[J].计算机技术与发展,2007,(07):123.
　WANG Jian-guang,DUAN Fu.A Method for Transformation from UML Model to XML Model[J].,2007,(10):123.
[2]赵立军.基于SysML的需求分析研究[J].计算机技术与发展,2011,(12):139.
　ZHAO Li-jun.Research on Requirement Analysis Based on SysML[J].,2011,(10):139.
[3]孙宏旭 邢薇 陶林.基于有限状态机的模型转换方法的研究[J].计算机技术与发展,2012,(02):10.
　SUN Hong-xu,XING Wei,TAO Lin.Research of Model Transformation Approaches Based on Finite State Machine[J].,2012,(10):10.
[4]李震,杨海亮,胡毅,等.需求工程对于软件开发的重要性[J].计算机技术与发展,2013,(03):199.
　LI Zhen,YANG Hai-liang,HU Yi,et al.Importance of Requirement Engineering in Software Development[J].,2013,(10):199.
[5]万小平,李蜀瑜.基于XML的UML模型向AADL模型的自动转换[J].计算机技术与发展,2014,24(03):71.
　WAN Xiao-ping,LI Shu-yu.Automatic Conversion of UML Model to AADL Model Based on XML[J].,2014,24(10):71.
[6]司旭光,王智学,何红悦. 智能通信业务的模型转换研究[J].计算机技术与发展,2015,25(01):199.
　SI Xu-guang,WANG Zhi-xue,HE Hong-yue. Study on Model Transformation of Intelligent Communication Service[J].,2015,25(10):199.
[7]孙健,徐敏. 基于AADL的嵌入式系统可调度性验证[J].计算机技术与发展,2016,26(03):23.
　SUN Jian,XU Min. Schedulability Verification of Embedded System Based on AADL[J].,2016,26(10):23.
[8]高正,曹子宁. 基于Z-AADL模型的形式化转换[J].计算机技术与发展,2017,27(03):23.
　GAO Zheng,CAO Zi-ning. Formal Transformation Basedon Z-AADL Model[J].,2017,27(10):23.
[9]李揭阳,李勇,张福高. 基于构件交互自动机的AADL模型转换方法研究[J].计算机技术与发展,2017,27(07):68.
　LI Jie-yang,LI Yong,ZHANG Fu-gao. Investigation on AADL Model Transformation Method Based on Component-interaction Automata[J].,2017,27(10):68.
[10]战芸娇,魏欧,胡军,等.面向驾驶舱显示系统需求的形式化建模与分析[J].计算机技术与发展,2018,28(03):20.[doi:10.3969/ j. issn.1673-629X.2018.03.005]
　ZHAN Yun-jiao,WEI Ou,HU Jun,et al.Formal Modeling and Analysis of Cockpit Display System Requirements[J].,2018,28(10):20.[doi:10.3969/ j. issn.1673-629X.2018.03.005]

更新日期/Last Update: 2019-10-10