● 摘要
机载软件是安全关键软件，对安全性和可靠性有着极高的要求。随着机载软件向高度综合化、模块化方向发展，机载软件系统设计日益复杂，代码量快速增长，现有的民用航空适航验证标准DO-178B无法融入不断涌现的诸如模型开发与验证、面向对象技术和形式化方法等软件开发的新技术。新的民用航空适航验证标准DO-178C对DO-178B进行了补充和修订，明确将形式化方法引入到机载软件的开发和验证过程中。
相较于传统软件开发方法，形式化方法使用严格的数学方法对软件进行开发，并对最终的软件系统进行形式化验证，从理论上保证软件的正确性，更能满足安全关键软件的安全性和可靠性需求。然而，现有形式化验证方法往往验证过程复杂，且对验证者的理论要求较高，对大规模软件的验证代价十分巨大。基于现有形式化验证方法实现的验证工具，虽然能在一定程度上提高形式化验证的效率，但其使用门槛较高，过度依赖人的交互证明，对循环程序的证明依赖于循环不变式的构造。
针对于现有形式化验证方法和形式化验证工具存在的问题，本文提出了一种基于语境的形式化验证方法，该方法以B*语言为形式规范语言，从程序的形式化描述推导出其形式化功能逻辑表达式，并通过对功能逻辑表达式正确性的验证完成对程序正确性的验证。该方法提出了语境的概念，用于记录程序证明的状态，辅助用户证明，并使用限定数学归纳法证明循环结构程序，避免了循环不变式的构造。本文基于提出的方法，实现了一个基于语境的形式化验证工具，该工具支持对非循环结构程序的自动证明，大大提高了验证的效率；支持对非循环结构程序的交互证明，能够引导用户给出循环的功能逻辑表达式，降低了证明难度。