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

摘要：

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

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

所属期刊栏目：29

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2019-10-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：153-156