中文摘要：

航空等领域中对安全关键软件的形式化验证有着迫切的需求，尤其关注存储安全性和正确性等特性。现实中的安全关键软件通常都采用多种语言共同实现，多语言编程使用非常普遍，而多语言接口部分常常是错误高发地带，而且也是目前研究的薄弱环节。为此，本项目以安全关键软件系统的完整形式化验证为远期目标，着重研究C语言与汇编语言这种具有代表性的多语言编程接口的形式化建模，以此为基础探索多语言编程的验证方法，并以广泛应用的开源嵌入实时操作系统为目标，开展原型系统验证研究。本项目将给出一种考虑多语言编程特征的程序建模和验证方法，解决其关键问题，为安全关键软件的构造提供技术支持。

结论摘要：

航空等领域中对安全关键软件的形式化验证有着迫切的需求，尤其关注存储安全性和正确性等特性。本项目以安全关键软件系统的完整形式化验证为远期目标，着重研究C 语言与汇编语言这种具有代表性的多语言编程接口的形式化建模，以此为基础探索多语言编程的验证方法，并以广泛应用的开源嵌入实时操作系统为目标，开展原型系统验证研究。本项目在汇编代码语义模型建模、出具证明编译器（certifying compiler）的设计与实现，以及出具证明编译器与验证汇编代码的结合验证等方面，已进行大量研究工作，本项目已经初步给出一种考虑多语言编程特征的程序建模和验证方法，为安全关键软件的构造提供技术支持，基本完成了预期的研究目标。在汇编语言的机器模型建模方面，本课题采用了验证汇编代码（certified assembly code）的方式，设计了基于x86指令集的一个抽象机器模型，该模型基于已有的工作CAP，且进一步考虑了对操作系统代码中出现的特定语义的支持；本课题设计并实现了一个出具证明的编译器PLCC，该编译器接受C的一个较大子集，生成验证机器代码，PLCC能够自动将标注在源代码层级的断言自动翻译到目标代码层并进行证明（基于PLCC编译器的一个变种已用于中国科学技术大学软件学院编译器课程的教学实践）；本项目设计并实现了出具证明编译器生成代码与手工构造的验证汇编代码联合验证的框架，在该框架中，自动生成的代码能够和手工代码及证明库进行联合验证和链接；本项目开始研究C/C++语言与JAVA接口的建模与描述，并着手构建工具原型，为多语言系统的安全性联合验证奠定了基础。