基于SysML的机载软件分层精化建模与验证方法

摘要

机载软件被广泛应用于航空航天领域,大幅提升了机载设备的性能.随着机载软件规模逐渐增大、功能逐渐增多,给软件的开发带来了难度.如何保障机载软件的正确性和安全性,也成为一个难题.基于模型的开发可以有效提升开发效率,而形式化方法能够有效保障软件的正确性.为了降低开发难度,同时保障机载软件的正确性、安全性,提出一种基于SysML状态机图子集的机载软件分层精化建模与验证方法.首先,使用SysML状态机图对机载软件的动态行为进行建模,根据提出的精化规则对初始模型进行手动逐层精化,得到精化设计模型;然后,针对软件模型动态变化的特性,将SysML状态机模型自动转换为时间自动机网络,并从软件需求中手动提取形式化TCTL性质进行模型检验.其次,为了实现编码自动化,将SysML模型自动转换至Simulink,利用Simulink Coder生成源代码.最后,以一个自动飞行控制软件为例进行了开发和验证,实验结果表明了该方法的有效性.