● 摘要
随着计算机技术的飞速发展，机载软件在民用航空领域得到广泛的应用，同时机载等安全攸关软件的开发也面临着巨大的挑战。现航空领域中主要采用的验证标准是美国航空无线电委员会（The Radio Technical Commission for Aeronautics，RTCA）提出的航空适航认证标准体系DO-178B以及DO-178C。DO-178C在原来DO-178B的基础上进行了补充，将形式化方法增加到了航空电子软件的开发和验证中。形式化方法使用软件规范形式语言对软件需求进行严格的形式化描述，采用形式验证技术从公理集及软件规范中推导软件需求。
和传统软件开发方法相比，形式化方法使用严格的数学方法对软件进行开发，并对最终的软件系统进行形式化验证，从理论上保证软件的正确性，更能满足安全关键软件的安全性和可靠性需求。然而，现有的形式化方法往往开发过程复杂，对使用者的理论要求比较高，使用门槛高，并且会产生大量的验证义务，增加开发难度。
针对现有的形式化方法存在的问题，本文提出一种新的形式化方法——B*，该方法以离散数学和计算机语言为基础，使用一阶数理逻辑及集合论开发和验证软件，确保正确性、鲁棒性、一致性以及安全性等，并用集合抽象具体的数据结构来简化开发和验证的难度，然后实现代码自动转换算法，将B*源程序转换到可执行代码。最后我们应用B*对安全实时分区操作系统标准ARINC653内核进行建模和实现。