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

• 作者: 宛伟健 葛晓瑜 邓刘梦
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 需求工程 模型转换 形式化验证 模型驱动开发
• 年，卷（期）: 2019,（10）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 153-156
• 页数: 4页
• 分类号: TP311
• 字数: 2830字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2019.10.030

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	葛晓瑜	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0
2	邓刘梦	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0
3	宛伟健	南京航空航天大学计算机科学与技术学院	2	0	0.0	0.0