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

来源：计算机技术与发展杂志2019年第10期北京时间：

作者：邓刘梦;葛晓瑜;宛伟健

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

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