航空航天道路交通等高安全领域的系统开发需要保证高安全、高可靠,对于该类系统的合理建模以及模型验证则尤为重要。当前模型驱动开发方法已经广泛应用于安全关键系统的开发过程中,它支持在早期就对系统进行安全分析和验证,有效地控制开发时间和成本,并降低系统出现风险的可能性。但与此同时,需求与设计模型之间仍然存在着沟壑,设计模型是否很好地满足用户所提出的需求在完成系统设计后仍需验证。针对系统建模语言缺乏精确形式化语义难以进行模型验证的问题,文中给出一套从SysML设计模型到NuSMV模型转换的语义规则,实现了一个自动转换程序,将SysML模型文件转换成NuSMV输入文件,进而利用NuSMV实现SysML模型的验证。最后通过一个铁路控制系统的案例证明了该方法的有效性。
类型: 期刊论文
作者: 邓刘梦,葛晓瑜,宛伟健
关键词: 需求工程,模型转换,形式化验证,模型驱动开发
来源: 计算机技术与发展 2019年10期
年度: 2019
分类: 信息科技,工程科技Ⅱ辑
专业: 铁路运输,计算机软件及计算机应用
单位: 南京航空航天大学计算机科学与技术学院
基金: 国家自然科学基金(617722770),南京航空航天大学开放基金(kfjj20171606)
分类号: TP311.52;U29-39
页码: 153-156
总页数: 4
文件大小: 1959K
下载量: 157
本文来源: https://www.lunwen66.cn/article/25ce9eeb9d453653f766f5b9.html