适航实时操作系统安全可靠的验证方案

DO-178C[[i]]在核心文档在DO-178B的基础上进行了重要改进，其中补充文档对特定的技术—软件形式化方法进行了详细的说明。DO-178C首次正式地承认了机载软件开发过程当中使用形式化方法的有效性。形式化方法是一类用于机载软件的规约、开发和验证的基于技术的数学方法，例如:形式化方法工具可以用来表达飞机上的数学表达控制原则以及它们到飞机计算机上的软件代码的转换。形式化方法可以应用到软件开发的多个阶段，也可以作为一种验证技术。

DO-178C标准对于软件开发和管理、验证提出了明确的目标和要求，并且提供了参考的方法。但是DO-178C标准并没有提出软件的验证的具体细节和流程。在实践中我们提出了具体的保障适航实时操作系统安全可靠的验证方案如图1所示。

在提出的这个方案中我们将验证方案从宏观方面分为两个部分：一个是DO-178C提出的验证，一个是软件形式化验证。

Do-178C提出的方案包括三个活动评审、分析和软件测试。其中，评审包括四个部分的评审：1）软件计划评审；2）软件需求、设计和代码评审；3）测试资料评审；4）其它资料的评审。评审的目的是保障软件的开发计划符合Do-178C的标准。其中，分析包括3个部分的分析：1）编码集成分析；2）基于需求的覆盖性分析；3）基于结构的覆盖性分析；分析是提供正确性的可重复证据的一种验证活动。其中软件测试包含基于需求的软件测试方法和保障软件正常和健壮性的测试用例的开发，软件测试的目的是揭示开发阶段制造的错误。由于所有的人类活动，尤其是复杂的活动都会引入错误，所以测试越严厉，我们就可以获得对产品质量的越大信心。通过对软件评审、分析、测试验证活动的执行，检测出软件存在的安全隐患，及时更改，使我们的软件达到满足适航的A级标准。

软件形式化验证部分，我们计划使用Coq一个基于高阶逻辑的定理证明工具验证系统的关键API，包括定时器中断处理程序（以及用于演示多级中断的支持的伪中断处理程序），调度程序，时间管理和四个同步机制：消息队列，邮箱，信号量和互斥体。

[[i]] DO-178C, Software Considerations in Airborne Systems and Equipment Certification[J].