航电系统软件可靠性的形式化验证技术研究

Ensuring the reliability and safety of the avionics software of civil aircrafts is a great challenge in the development of modern avionics systems. According to DO-178C, the de facto international standard for airworthiness certification, it is suggested to apply formal methods and model-based development and verification, to ensure reliability and safety. This project aims at studying model checking and runtime verification, two main stream formal verification techniques, by integrating the special features of avionics software. We will first propose a new formal specification language for precisely describing the correctness properties that must be satisfied by the models, which are written in UML, SysML, AADL or Lustre, and the source code, which is written in embedded C language, of avionics software. Then we will prove the decidability, monitorability and expressiveness of the new specification language by theoretical analysis, and we aim at a specification language which is more avionics-oriented and more expressive than the existing specification languages. Finally, we will develop algorithms for verifying these specifications and generating counter-examples, both for software models and source code, and develop verification tools. As a result, this project can cover the verification requirements of the development process of avionics software, raise the level of verification automation, decrease the faults in software, improve the software quality, and provide strong technical support for airworthiness certification.

确保民用飞机航电系统软件的可靠性与安全性是现代航电系统开发中面临的重大挑战。根据国际权威的适航认证标准DO-178C，为了确保航电软件的可靠性与安全性，要求使用形式化验证方法和基于模型的验证方法。本项目主要针对航电软件的领域特征，研究模型检验和运行时验证这两种主流的形式化验证技术：首先提出一种新的针对航电软件模型和代码的形式化规约语言，用于准确描述UML、SysML、AADL、Lustre等航电软件模型和嵌入式C程序必须满足的正确性性质；然后通过理论分析，证明新的规约语言的可判定性、可监测性和表达能力，以期获得比现有规约语言更有航电软件领域特征、表达能力更强的规约语言；最后，在软件模型层次和代码层次上，针对该规约语言设计形式化验证算法及其反例生成算法，并开发验证工具，从而实现覆盖航电软件开发过程的全面验证，提升验证的自动化程度，减少软件缺陷，提高软件质量，并为适航认证提供有力的技术支持。

确保民用飞机航电系统软件的可靠性与安全性是现代航电系统开发中面临的重大挑战。根据国际权威的适航认证标准DO-178C，为了确保航电软件的可靠性与安全性，要求使用形式化验证方法和基于模型的验证方法。本项目主要针对航电软件的领域特征，研究模型检验和运行时验证这两种主流的形式化验证技术。本项目的主要研究内容和重要结果包括：.（1）我们提出了一种新的规约语言，用于准确描述航电软件必须满足的正确性性质，用户可以方便地针对程序中的事件定义基于线性时序逻辑和模式语言的形式化规约，该规约语言为用户提供了一种与验证工具交互、可以方便而准确地表达待验证性质的方式；.（2）我们提出并实现了规约语言的可满足性和可监测性判定算法，并证明了针对正则语言的参数化运行时验证问题的计算复杂度为NP完全的，解决了规约语言判定算法和验证问题计算复杂度方面的若干开放问题；.（3）我们研究了针对Lustre模型的模型检验算法。我们可以通过实现显式状态模型检验算法生成模型的状态空间，然后使用偏序约减技术在验证过程中对状态空间进行约减；也可以将模型转化为逻辑公式，然后调用SAT/SMT求解器对逻辑公式求解，得到验证结果；.（4）我们研究了针对C代码的运行时验证算法，被验证的正确性性质包括通用性质和用户自定义性质，该算法可以用于构造C程序的运行时验证工具，应用于对航电软件代码的验证，提升验证的自动化程度，减少软件缺陷，提高软件质量；.（5）本研究展示了模型检验对机载软件适航认证的支持，例如提供证据证明高级需求与低级需求的一致性、低级需求与软件模型的一致性、以及软件模型与代码的一致性，可以为机载软件的安全性保障和DO-178C/DO-333适航认证提供技术支持；我们提出使用源到源的转换来实现动态分析工具，由于插桩后文件是源代码形式，因此可以依照DO-178C的标准对它进行代码审查、分析和验证，从而达到适航认证的要求。