> >网站资源
．．> >图书馆:TechXchange
. . . .>> TechXchange:嵌入式软件
.. .. .. >>主题：ADA和Spark
开发安全可靠的系统可能是一项具有挑战性的任务，但是使用正确的工具可以使其变得更容易。许多这样的工具，如静态分析，可以应用于像C和c++这样天生缺乏这种支持的语言，而不是像这样的语言火花和铁锈它们将这些技术作为其定义的一部分，使它们可用所有使用该语言的程序员．
Spark是ADA 2012的一个子集，额外的英里，具有可提供的静态分析，但利用其所有优点可能是令人生畏的。尽管如此，这些功能的增量使用可以提供显着的好处，并且使用它们的子集可能适用于许多情况。这类似于C和C ++的Misra支持，这是一个可以选择性地应用于许多项目的规则集合。屠杀和其他编码标准提供一种提高程序员创建的代码质量的方法。
《SPARK应用实施指南》白皮书由Adacore和泰利斯公司在美国，两家公司涉及高保证系统。它提出了在高保证开发环境中使用SPARK的多层方法。论文中列出的级别包括:
- 石头 - 有效的火花代码
- 青铜-初始化和正确的数据流
- 银-没有运行时错误
- 金-密钥完整性属性的证明
这并不是第一个使用这种命名约定的系统。英特尔最新的处理器系列也走了这条路吗．
请参阅该论文以获取详细信息，因为在这里可以涵盖更广泛的描述和示例。这些示例是用Ada/SPARK编写的，原因很明显，但它们也可以指导那些使用不同平台的人，以突出创建高安全性应用程序的常见问题。
有很多关于艾达的神话，大多数嵌入式程序员对SPARK的了解甚至更少其中c和c ++主宰．使用好的工具和编码标准可以显著减少开发程序过程中产生的bug数量，而不会显著增加创建应用程序所花费的时间。事实上，开发一个安全的应用程序所需的时间实际上比使用非结构化方法创建应用程序所需的时间要少。
