经验报告 - SCADE Suite 6 KCG 经历 DO-178B 认证过程中进行的活动

详细内容可参考 ICFP’09 《Experience Report: Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework》。

数十年前，民用航空电子机构就定义了机载嵌入式代码的认证要求。DO-178B 标准（RTCA/DO-178B，1992）规定了机载软件开发的限制约束。该流程
已被纳入航空器的全周期认证流程中。目前在与关键软件有关的其他工业领域（医疗行业的 FDA Class III、铁路应用的 EN 50128、汽车行业的 IEC 61508 等）也有相应的认证程序。

Esterel Technologies 推广的 SCADE Suite 6 是一种基于模型的开发环境，专用于高安全嵌入式软件。该套件的代码生成器 (KCG) 可将模型转化为符合 DO-178B 标准的嵌入式 C 代码。通过使用 KCG，开发安全关键嵌入式应用程序最终用户可以通过免于验证生成的代码是否与 SCADE 模型一致，从而降低开发成本。如此，验证和确认活动减少了，只需证明模型符合嵌入式应用的功能要求即可。

该编译器的第一个版本是用 C 语言实现的，于 1999 年发布。该编译器基于当时用程序语言 Eiffel的变种（LOVE）编写的代码生成器（ECMA 2005）所开发，当时出于避免被认证机构拒绝的缘故，因此用 C 语言重新编实现了该编译器。

之后，自 2001 年起，Esterel Technologies 开始研究新的编译技术和语言扩展。该工作旨在证明，采用类型系统等方法对语言进行设计，并使用OCaml进行实现，在产业项目角度也是一种高效而清晰的方法。目前的经验显示出，OCaml可以显著缩小工程工具的规范和实现之间的距离，更好地追踪工具输入语言的形式化描述与其编译器实现之间的关系。因此，Esterel Technologies 使用 OCaml 设计了其新的 SCADE SUITE 6。

本文将介绍 Esterel Technologies 为使 KCG 通过以下几项规范的认证而进行的具体开发活动: DO-178B、IEC 61508 和 EN 50128。这些标准的差异和特殊性不在本文讨论范围之内；为方便起见，我们重点讨论美国联邦航空局标准（DO-178B，level A）。详细内容可参考 ICFP’09 《Experience Report: Using Objective Caml to Develop Safety-Critical Embedded Tools in a Certification Framework》。