> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
. . . . . .>>主题:Ada和SPARK
安全可靠的软件是使用良好的工具和设计来构建的，这些工具和设计能够交付尽可能没有bug的代码。Ada和火花这是一种旨在减少漏洞数量的编程语言，通常被用于要求高可靠性和安全性的航空电子设备等领域。Ada和SPARK也非常适合微控制器级别的嵌入式设备，比如Arm Cortex-M，在这种级别上，高效的代码至关重要。
由于认证的重要性，航空电子应用程序也经常利用Ada和SPARK工具。然而，工具成本上升到较高的水平，并且工具的认证是开发过程的一个方面。向后兼容性和长期支持也很关键。
AdaCore的GNAT Pro工具套件一直支持Ada和SPARK，并支持C和c++开发，就是为了解决这些成本问题而创建的。AdaCore最近改进并将产品线划分为四个版本:GNAT Pro Assurance、GNAT Pro Enterprise、GNAT Pro Developer和免费、开源的GNAT Pro社区。
保证和企业
保证和企业版针对的是AdaCore的现有客户，这些客户需要对多个版本的长期支持，并需要访问持续的补丁版本。保证版提供了持续的分支支持，允许向客户提供非常具体的支持。它还提供认证服务。
保证和企业版本支持Ada 83, Ada 95, Ada 2005，以及最新版本Ada 2012，以及SPARK。C和c++支持是可选的。Developer版本支持C、Ada 2012和SPARK。
开发人员和社区
新的开发者版本针对新的Ada和SPARK开发者。当然，希望学习或试验Ada和SPARK的开发人员可以使用免费的Community版本，但是Developer版本对于商业开发是有意义的。它的价格与商业C/ c++开发套件相当。它提供了对连续补丁版本的直接支持和访问。社区版本得到更新，但更新周期较长。
开发平台包括Linux、macOS和Windows，它们也是目标。此外，Enterprise和Assurance版本支持Solaris和AIX。跨平台支持包括Android、PowerPC Linux、iOS、Lynx178、PikeOS和VxWorks。所有版本都支持裸金属Arm平台以及嵌入式Linux。除了社区版，其他版本都支持QNX。这是非常重要的，因为QNX被用于高可靠性和安全性的应用领域，如汽车。
工具包有一系列的工具，包括GNATbench和GNAT Programming Studio ide。其他有趣的特性包括Ada Web服务器(AWS)、gnaxis和GNATemulator。
的火花的发现该工具是这个包的一部分，针对的是刚接触SPARK和正式方法的开发人员。Ada 2012增加了SPARK合同，用于对应用程序进行静态、正式的验证。这允许开发人员证明应用程序符合规范。C和c++程序的认证通常是通过过程和测试来完成的，而不是对代码使用正式的方法。
例如，Pre和Post条件是可以应用于函数的契约，如Ada 2012/SPARK代码片段所示:
这本质上迫使Insert函数要求Last变量在调用之前和之后都是Queue的有效索引。这可以通过编译器或运行时检查来检查。使用形式化的方法来检查整个程序可以消除检查。
当然，使用这些类型的正式方法需要额外的工作，但是在高安全性的应用程序中往往需要这样做。通过减少应用程序中的错误数量和减少检查开销，它在一般的嵌入式应用程序开发中也非常有用。
开发人员和应用程序不需要利用SPARK的全部功能来启动。泰利斯和AdaCore合并“SPARK实施指南指南，从使用SPARK的角度阐述了多个复杂级别。它从Stone开始，它本质上是有效的SPARK代码，接着到Gold，它在整个过程中都使用了契约和证明。SPARK Discovery工具可以与本指南结合使用。
与最流行的嵌入式语言(如C、c++和Java)相比，Ada和SPARK开发人员更少。尽管如此，学习Ada和SPARK还是相对简单的。许多神话都与艾达有关,但即使是新手也可以很快学会使用这些工具进行编程．
希望为应用程序开发安全、安全、无bug代码的公司应该考虑使用Ada和SPARK的优点。现在开始更经济了。
