哪些语言用于安全关键软件？
我正在研究安全关键型软件的开发，特别是编程语言select对这种开发有什么影响。
请详细解释哪些语言是常用的，为什么。
Ada和SPARK （这是一种用于静态validation的Ada方言）被用于航空航天领域，用于构build诸如航空电子系统等高可靠性软件。 这些语言有一些代码validation工具的生态系统 ，尽pipe这种技术也适用于更多的主stream语言 。
Erlang是从头开始 编写高可靠性电信代码的。 它旨在便于分离错误恢复问题（即生成错误的子系统与处理错误的子系统不同）。 虽然这个能力还没有真正走出研究圈子，它也可以受到正式的certificate。
由于语言的声明性 ， Haskell等函数式语言可以通过自动化系统进行forms化的certificate。 这允许带有副作用的代码被包含在一元函数中。 对于一个正式的正确性certificate，其余的代码可以被假定为什么都不做，只是指定了什么。
但是，这些语言是垃圾收集的，垃圾收集对代码是透明的，所以不能以这种方式推理。 垃圾收集语言对于硬实时应用程序来说通常是不够可预测的，尽pipe在时间有限的增量垃圾收集器方面正在进行一系列研究。
Eiffel及其后代已经内build了一个名为Design By Contract的技术支持，该技术提供了一个强大的运行时机制来整合不variables的前后检查。 虽然Eiffel从来没有真正被抓住过，但是开发高可靠性软件往往是在编写function之前先编写检查和处理失败模式的处理程序。
尽pipeC和C ++并不是专门为这种types的应用程序devise的，但出于多种原因，它们被广泛用于embedded式和安全关键型软件。 注意的主要属性是控制内存pipe理（例如，可以避免垃圾收集），简单，debugging良好的核心运行时库和成熟的工具支持。 目前使用的很多embedded式开发工具链最早是在20世纪80年代和90年代开发的，当时这种技术是当时stream行的Unix文化，所以这些工具在这类工作中仍然很受欢迎。
虽然必须仔细检查手动内存pipe理代码以避免错误，但是它允许对应用程序响应时间进行一定程度的控制，而这对于依赖于垃圾回收的语言是不可用的。 C和C ++语言的核心运行时库相对简单，成熟和易于理解，因此是最稳定的平台之一。 大部分（如果不是全部）用于Ada的静态分析工具也支持C和C ++，还有许多其他的可用于C的工具 。 还有几个 广泛 使用的 基于 C / C ++ 的 工具 链 ; 用于Ada的大多数工具链也都支持C和/或C ++版本。
诸如公理化语义 （PDF）， Z符号或通信连续过程之类的forms化方法允许对程序逻辑进行mathvalidation，并经常用于安全关键软件的devise中，其中应用程序足够简单以应用它们（通常是embedded式控制系统） 。 例如， 我以前的一位讲师为德国铁路网做了一个正式的信号系统的正确性certificate。
forms化方法的主要缺点是它们倾向于在被certificate的基础系统方面复杂度呈指数级增长。 这意味着证据中存在很大的错误风险，所以它们实际上仅限于相当简单的应用。 forms化方法被广泛用于validation硬件的正确性，因为硬件错误的修复非常昂贵，尤其是在大众市场产品上。 自从Pentium FDIV出现问题以来，正式的方法已经引起了很多的关注，并被用来validation自Pentium Pro以来所有Intel处理器上FPU的正确性 。
许多其他语言已被用来开发高度可靠的软件。 对这个问题进行了大量的研究。 人们可以合理地认为方法论比平台更重要，尽pipe有简单性，select和控制依赖性等原理，可能会排除使用某些平台 。
正如其他人已经注意到的，某些操作系统平台具有提高可靠性和可预测行为的function，例如看门狗定时器和有保证的中断响应时间。 简单性也是可靠性的强大驱动力，许多RT系统都被故意保持非常简单和紧凑。 QNX （我所熟悉的唯一一个这样的操作系统 ，曾经使用过一个基于它的混凝土配料系统 ）非常小，可以装在一张软盘上。 出于类似的原因，制作OpenBSD的人（也就是其强大的安全性和全面的代码审计function）也使得系统变得简单。
编辑： 这篇文章有一些关于安全关键软件的好文章的链接，特别是这里和这里 。 支持S.Lott和Adam Davis的来源。 THERAC-25的故事在这个领域是一个经典的作品。
对于C ++，联合攻击战斗机（F-35）C ++编码标准是一个很好的解读：
我相信Ada仍然在一些安全和/或任务关键的政府项目中使用。 我从来没有使用过这种语言，但是和埃菲尔一起，这是在我的“学习”清单上。 Eiffel提供Design By Contract，旨在提高可靠性和安全性。
首先，安全关键软件遵循您在传统机械和电气工程领域将会看到的相同原则。 冗余，容错和故障安全。
另外，正如前面的招贴画所暗示的那样（这是因为某种原因而被低估的），能够做到这一点的一个最重要的因素就是让你的团队对所发生的一切有一个坚定的理解。 不言而喻，您的好软件devise是关键。 但是这也意味着一种可以获得的，成熟的，得到很好支持的语言，对此，有许多共同的知识和经验丰富的开发人员。
许多海报已经评论说操作系统是这方面的一个关键因素，这是非常正确的，因为它必须是确定性的（见QNX或VxWorks）。 这就排除了大多数在幕后为你做事情的解释性语言。
ADA是一种可能性，但是那里没有工具和支持，更重要的是恒星人不是那么容易获得的。
只有你严格执行一个子集，C ++才是可能的。 在这方面，这是魔鬼的工具，承诺让我们的生活更轻松，但往往做得太多，
C是理想的。 它非常成熟，快速，拥有多样化的工具和支持，许多经验丰富的开发人员，跨平台，非常灵活的，可以接近硬件。
我已经从smalltalk发展到ruby，欣赏和享受高级语言所提供的一切。 但是当我进行关键系统开发的时候，我咬紧牙关，坚持使用C语言。根据我的经验（防御和许多II类和III类医疗设备），更less。
如果它比其他任何东西都安全的话，我会拿起哈斯克尔的。 我build议haskell，因为它具有非常严格的静态types检查，它促进编程的地方，你很容易testing。
但是我不会太在意语言。 您可以获得更高的安全性，而不会因为您的项目整体状况良好而没有最后期限地工作。 总体而言，就像所有的基本项目pipe理一样。 我可能会专注于广泛的testing，以确保一切工作，它应该，testing覆盖所有angular落案件+更多。
语言和操作系统是重要的，但devise也是如此。 尽量保持它的骨子，简单的死亡。
我将首先获得最less的状态信息（运行时数据），以尽量减less不一致的机会。 那么，如果你想要容错的冗余，确保你有万无一失的方法来恢复数据不一致。 没有办法从不一致恢复的冗余只是要求麻烦。
当请求的行为在合理的时间内没有完成时，总是有一个回退。 正如他们在空中交通pipe制中所说的那样，一个未经确认的通关是不能通过的。
不要害怕投票的方法。 它们简单可靠，即使可能浪费几个周期。 避开只依赖于事件或通知的处理，因为它们可能容易被丢弃，重复或错误。 作为投票的辅助手段，他们很好。
我在APOLLO项目上的一位朋友曾经说过，他知道，即使计算机速度非常慢，他们决定依靠投票而不是事件，情况变得严重。
PS我刚刚阅读了C ++的飞行器标准。 他们没问题，但他们似乎认为会有很多类，数据，指针和dynamic内存分配。 这正是不应该超过绝对必要的。 应该有一个大镰刀的数据结构沙皇。
操作系统比语言更重要。 使用实时内核，如VxWorks或QNX。 我们考虑了两个控制工业机器人，并决定采用VxWorks。 我们将C用于实际的机器人控制。
对于真正关键的软件，例如飞机自动着陆系统，您需要独立运行的多个处理器来交叉检查结果。
实时环境通常具有“安全关键”要求。 对于这样的事情，你可以看看VxWorks ，一个stream行的实时操作系统。 它目前在波音飞机，宝马iDrive内部，RAID控制器和各种航天器等许多不同领域使用。 （ 检查出来 ）
VxWorks平台的开发可以使用多种工具完成，其中包括Eclipse ， Workbench ， SCORE等。 C，C ++，Ada和Fortran（是，Fortran）以及其他一些支持。
既然你不给平台，我不得不说C / C ++。 在大多数实时平台上，无论如何，选项相对有限。
C的倾向，让你自己在脚下自己的缺点被validation代码的工具的数量以及代码与平台的硬件能力的稳定性和直接映射所抵消。 而且，对于任何关键的问题，您将无法依赖尚未广泛审查的第三方软件 – 这包括大多数库 – 甚至硬件供应商提供的许多库。
由于一切都将是你的责任，你需要一个稳定的编译器，可预测的行为和一个紧密的映射到硬件。
这里有一些工具的更新，我还没有看到，我最近一直在玩，这是相当不错的。
LLVM Compiler Infrastructure（LLVM编译器基础架构 ）是他们主页上的短文（包括用于C和C ++的前端，用于Java，Scheme和其他语言的前端正在开发中）。
编译器基础架构 – LLVM也是实现语言和编译策略的源代码集合。 LLVM基础架构的主要组件是基于GCC的C＆C ++前端，具有不断增长的全局和过程间分析和转换的链接时间优化框架，用于X86，X86-64，PowerPC的静态后端32/64，ARM，Thumb，IA-64，Alpha，SPARC，MIPS和CellSPU架构，发射可移植C代码的后端以及用于X86，X86-64，PowerPC 32/64的即时编译器处理器和MSIL的发射器。
VCC ;
VCC是一个工具，certificate注释的并发C程序的正确性或发现问题。 VCC通过契约function来deviseC，包括前置和后置以及types不变式。 带注释的程序使用Boogie工具转换为逻辑公式，将其传递给自动SMT解算器Z3以检查其有效性。
VCC使用最近发布的通用编译器基础结构 。
LLVM或VCC这两种工具都被devise为支持多种语言和体系结构，我认为它们是通过契约和其他正式validation实践进行编码的一种增长。
WPF （不是MS框架:)是一个很好的开始，如果你想在程序validation领域评估一些最近的研究和工具。
WG23是主stream资源，但是对于相当具体的关键系统开发语言细节 。 它们涵盖了Ada，C，C ++，Java，C＃，脚本等方面的所有内容，至less有一套体面的参考和指导方针来更新有关语言特定缺陷和漏洞的信息。
一种使用谨慎模式的语言可能会有所帮助，但是您可以使用任何语言，甚至是汇编语言来强加谨慎的模式。 关于每个价值的每一个假设都需要testing假设的代码。 例如，总是在除数之前testing除数为零。
您可以信任的可重用组件越多，任务就越容易，但可重用组件很less被authentication用于关键用途，也不会让您通过法规安全stream程。 你应该使用一个微小的操作系统内核，然后构build一个随机inputunit testing的小模块。 像艾菲尔这样的语言可能会有帮助，但是没有银弹。
在http://www.dwheeler.com （“高保证软件”）有很多很好的参考资料。
对于汽车产品，请参阅MISRA C标准。 C但是你不能使用两个以上的指针级别，以及其他一些类似的东西。
adahome.com在Ada上有很好的信息。 我喜欢这个C ++到Ada教程： http : //adahome.com/Ammo/cpp2ada.html
Tom Hawkins做了一些有趣的Haskell工作。 请参阅：ImProve（语言合并SMT解算器来检查validation条件）和Atom（EDSL硬实时并发编程，而不使用实际线程或任务）。
任何软件产品都可以使用任何工具通过DO-178bauthentication过程，但问题是多么困难。 如果编译器没有通过authentication，您可能需要certificate您的代码在汇编级别是可追踪的。 所以你的编译器被authentication是有帮助的。 我们在项目中使用了C，但必须在程序集级别进行validation，并使用代码标准，包括closures优化器，有限的堆栈使用，有限的中断使用，透明的可certificate的库等.ADA不是精灵，但是它使得PSAC计划看起来更可行。
随着应用程序变大，汇编代码变得不太可行。 ARM处理器只是邀请C ++，但是如果你问Kiel这样的公司，他们的工具是否通过authentication，他们会回来“呃？ 不要忘记，validation工具也需要authentication。 尝试validation一个LabViewtesting程序。
我不知道我会用什么语言，但我知道我不会用什么语言：
有关JAVA支持的说明。 该软件产品可能包含对JAVA书面程序的支持。 JAVA技术不是故障容忍的，并不是devise，制造，或者意图在危险环境中使用或转售的在线控制设备，要求安全性能，例如在操作核设施，飞机导航或通信系统，AIR交通pipe制，直接生命支持机器或武器系统，其中Java技术的失败可能直接导致死亡，人身伤害或严重的物理或环境损害。
HAL / S用于航天飞机。
目前正在开发一个新的Java安全关键标准 – JSR 302：安全关键Java技术 。
安全关键Java （SCJ）是基于RTSJ的一个子集。 目标是build立一个适用于安全关键authentication安全关键程序（DO-178B，A级和其他安全关键标准）的开发和分析的框架。
例如，SCJ删除了RTSJ中仍然存在的堆，它还定义了3个合规级别，应用程序和VM实现可以符合，合规级别被定义为简化各种复杂应用程序的authentication。
资源 ：
- 用于安全关键应用程序的Java。
- JSR 302：安全关键Java技术
- 用Java开发安全关键型应用程序
由于很多原因，Java是一种非常重要的语言。 它是由一个白痴devise的，他误解了Wirth教授的Pascal和Oberon项目。
ADA是一个由大型委员会devise的语言，由此产生的蔓延使我想起了PL / 1，这非常棒，但编写一个编译器如此复杂，以至于没有人会提起它。
Modula-2可能是有史以来最简单的语言，而不是C，我使用了代码大小为一半的modula-2（因此运行速度快两倍）。 C只是汇编程序的一个步骤，只是通过呼吸太困难，你可以创build一个讨厌的bug。
帕斯卡和基本是非常可靠的语言。 事实上，Visual Basic 6编译器/工具包可能是MS曾经生产过的最好的东西，人们仍然在MS放弃它15年后才使用它。 不要让我开始讨厌.NET这个可憎的东西，这是MS出来的最糟糕的一堆垃圾，它想要创build一个没有人可以克隆的专有系统。 太糟糕了，没有人想克隆它！ 他们成功地做了一些模糊的事情。
Eiffel本质上是可靠的，因为它使用了子任务结束时自己堆栈和堆栈的小subprocess，所以你不会片段化内存。 但好运理解艾菲尔，这是一个疯子的工作。 米兰达（Miranda）也是如此，还有那些由math怪胎devise的学术语言，而不是那些习惯于实践的人。
我会说Python是最好的语言之一。 易于阅读，快速，简单。 它不是特别安全，但是对于脚本来说，它打败了Bash shell脚本，或者天堂禁止的叫做Perl的残酷的只写语言。
