题目：基于软件规范形式语言证明算法与程序变换的研究与实现

大型飞机机载软件是安全攸关软件，对正确性、安全性、可靠性有着极高的要求。而随着机载软件日益向高度综合化、模块化以及复杂化的方向发展，以DO-178B为首的机载软件适航验证标准无法完全覆盖不断涌现的诸如面向对象技术、形式化方法等软件开发新技术，于是在2012年提出了修改版的DO-178C。在DO-178C中，形式化方法被首次正式引入。形式化方法能够对机载软件程序进行严格的证明，保证正确性，然而它对使用者的理论基础要求较高，且在证明过程中会消耗大量人时，难以用于规模验证。

现有的形式化方法在形式化验证工具的辅助下，在一定程度上提高了验证效率，但其使用的形式规范表述程序较为复杂，依赖人为构造循环不变式，降低了证明效率。本文的研究目标是研究现有的形式规范和验证工具，采用从程序的形式规范推导其形式化逻辑功能描述和使用数学归纳法取代循环不变式的方法设计并实现正确高效的形式化方法及其验证工具，提高形式化证明的效率。论文的主要工作包括以下几个方面：

1、从大型飞机安全攸关机载软件的安全可靠性需求出发，阐述了使用形式化方法验证机载软件的价值，并分析了降低形式化方法的难度、提高验证的效率的意义。

2、 分析了典型形式化方法的理论、形式规范以及工具的特点，给出B*软件规范形式语言的具体设计和基于语境的形式化证明方法的理论基础、语义学以及证明策略的设计，提出了新的能够提高形式化验证效率的形式化证明思想。

3、 为基于语境的形式化证明方法的理论设计详细的证明算法。将证明序列中的证明项使用树形数据结构表示，通过对证明项的树形结构进行修改来实现不同的证明策略算法，简化了证明策略的设计并为用户提供了自定义证明策略设计的接口。

4、 结合机载软件需求、B*程序规范和基于语境的形式化证明方法，设计并实现形式化验证工具，并进行验证。结果表明，本文提出的方法和实现的工具正确地对软件需求的正确性进行了证明，并且有效地降低了使用难度和证明成本，提高了证明效率。

本文设计并实现的软件规范形式语言B*以及支持B*语言和基于语境的形式化方法的验证工具有以下特点：可以从程序的形式规范推导其形式化逻辑功能描述，半机械地对程序进行证明；使用数学归纳法取代循环不变式，避免在循环的证明中人为构造循环不变式；B*语言更易理解与使用；形式化验证工具使用简单，证明效率高。