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

注：因版权方要求，不能公开全文，如需全文，请咨询杂志社