基于NuSMV的SysML模型形式化验证  

Formal Verification of SysML Model Based on NuSMV

作　　者：邓刘梦 葛晓瑜 宛伟健 DENG Liu-meng;GE Xiao-yu;WAN Wei-jian(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院

出　　处：《计算机技术与发展》2019年第10期153-156,共4页Computer Technology and Development

基　　金：国家自然科学基金(617722770);南京航空航天大学开放基金(kfjj20171606)

摘　　要：航空航天道路交通等高安全领域的系统开发需要保证高安全、高可靠,对于该类系统的合理建模以及模型验证则尤为重要。当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制开发时间和成本,并降低系统出现风险的可能性。但与此同时,需求与设计模型之间仍然存在着沟壑,设计模型是否很好地满足用户所提出的需求在完成系统设计后仍需验证。针对系统建模语言缺乏精确形式化语义难以进行模型验证的问题,文中给出一套从SysML设计模型到NuSMV模型转换的语义规则,实现了一个自动转换程序,将SysML模型文件转换成NuSMV输入文件,进而利用NuSMV实现SysML模型的验证。最后通过一个铁路控制系统的案例证明了该方法的有效性。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.

关 键 词：需求工程 模型转换 形式化验证 模型驱动开发 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]