2018年8月12日 • 航空航天和国防

可靠、安全、可靠?Ada和VxWorks可以帮助!

由Guest Conderstor Ben Brosgol，高级技术人员，骗子

编写可靠、安全和可靠的软件是困难的。对于具有严格认证要求的硬实时系统，如航空电子设备的DO-178B或DO-178C，则更困难，而且确实是开发者必须面对的最艰巨的挑战之一。要应对这一挑战，需要经验丰富的编程语言、开发工具和目标平台支持:AdaCore和风河自2001年公司订立正式合作伙伴关系以来一直提供我们的联合客户。利用ADA语言和一个广泛的工具集风河的工作台IDE，应用程序开发人员可以在一系列中以最高级别的安全临界性生产软件VxWorks平台和处理器系列。

涂层/风河开发环境在航空航天和国防工业中拥有悠久而强大的血统。展示的应用程序包括：

涂层/风河合作伙伴如何帮助您？

《美国残疾人法》的语言

Ada本身带来了许多好处。作为一种现代的通用语言，Ada具有强大的类型检查功能，可以在错误变成运行时错误之前早期检测和纠正错误——在许多情况下是在编译时。它具有您所期望的高级功能:面向对象、通用模板、异常处理、数据抽象、并发性(任务处理)、扩展标准库等。该语言的最新版本支持“基于契约的编程”，实际上，它在源代码中嵌入了需求，在源代码中可以动态(通过测试)或静态(通过适当的工具支持)验证需求。Ada还提供了底层编程所需的特性;您可以用Ada编写中断处理程序、指定数据表示和对齐、管理字节序问题、与C进行接口，并且通常可以像在汇编程序中那样对硬件进行尽可能多的控制。

AdaCore工具

一种语言的好坏取决于它的工具支持，对于Ada来说，一个广泛的工具集，与Wind River的Workbench IDE顺利集成，加速了软件生命周期的开发和验证过程。静态分析工具包括一个堆栈使用计算器、一个编码标准执行者、一个度量报告器和一个兼容cwe的“bug查找器”。对于最关键的应用程序，基于可正式验证的SPARK语言(Ada的子集)的证明技术可以证明程序的属性，如没有运行时错误、安全策略一致性，甚至完全功能正确性。对于动态分析，覆盖工具可以确定到MC/DC的源代码覆盖，而测试工具生成器可以简化测试套件的组织和管理。在DO-178B (DO-178C中的TQL-4或TQL-5)中，有一些工具已被确认为验证工具，通过自动化活动来降低认证成本，否则将需要手工完成。

VxWorks RTOS.

adacore的gnat pro编译器将Ada的动态功能有效地将Ada的动态功能映射到底层VxWorks服务，允许开发人员利用语言的高级构造而不会牺牲性能。除了完整的ADA运行时间库外，还有几种专用配置文件，可特别适用于安全关键应用程序。例如：

ZFP(零占用空间)配置文件包含最小的运行时代码。
CERT配置文件将ZFP扩展到VxWorks 653上的ARINC-653 APEX进程的功能，包括支持ARINC-653 APEX进程。此配置文件实现了未来空中能力环境（FACE™）标准的ADA安全基础和安全性能集。
Ravenscar Cert Profile通过支持Ravenscar Tasking Subset来增强证书简介。它提供了面部标准的ADA安全扩展功能集所需的功能。

这些配置文件已经实现了风河的面部一致的VxWorks 653 V2.5 RTOS，也为VxWorks 653 V3.x。

GNAT Pro ADA开发环境现已用于ARM 64位上的VxWorks 7 RTOS，PowerPC 64位和英特尔32位多核架构。这些发行添加到VxWorks 7目标（ARM 32位，PowerPC 32位和Intel 64位），VxWorks 6和VxWorks 653的现有GNAT Pro支持。

底线

生产、认证和维护关键安全应用程序是一项艰巨的任务，需要一流的语言、工具和RTOS技术。AdaCore和Wind River已经满足这一需求近20年，为VxWorks平台提供Ada环境，帮助客户将风险和成本降至最低。虽然开发和验证问题很困难，但解决方案的决定很容易:选择Ada和VxWorks，并确保您的软件可以放心地运行。