为什么光泽被用于编程关键控制软件(核电厂等)？

Question

因此，正如维基百科所述：

Lustre是一种正式定义、声明性和同步的数据流编程语言，用于对反应性系统进行编程。它始于20世纪80年代初的一个研究项目。该语言的正式介绍可在1991年IEEE会议记录中找到。1993年，由Esterel技术公司开发的以工业环境SCADE为核心语言的商业产品的实用化、工业化应用。它现在用于飞机、直升机和核电站的关键控制软件。

我想知道为什么像这样的语言会被用于关键控制软件，以及它们为什么会被开发。例如，它可以用C编写吗？

为什么需要设计这种特定的语言？是因为它们“更快”，还是因为它们是专为它们所在的系统而设计的？

Answer 1

为什么像这样的语言(光泽)被用于关键控制软件。

因为一些软件工具(甚至方法学)可以帮助部分证明代码w.r.t的正确性。一些形式化的规范，以及其他一些(或相同的，例如SCADE)软件工具可以从光泽源生成一些C代码(这将是“更安全的”，也许比手写代码所能实现的更快)。

阅读关于静态源程序分析的文章。

请注意，有一些工具可以帮助证明某些C程序(具有受限的编码风格)在某种程度上是“安全的”或“正确的”w.r.t。一些形式化的规范；例如查看Frama-C。

另外，请记住，一些编程语言子集(例如，Ocaml的大部分，感谢它的类型系统，但没有它臭名昭著的Obj.magic把戏)可以通过设计“保证”您的程序不会崩溃(w.r.t )。某些假设)。

但请记住:有没有银弹：由于停止问题的不可分辨性，您不可能希望完全证明任何软件(您也不能希望将其规范和环境完全形式化；您需要接受软件是抽象的.)

也可以阅读拉特纳的博客：每个C程序员都应该知道什么是未定义的行为

顺便说一句，几个行业(包括核工业，飞机，甚至医疗器械等)有关于安全关键软件的规范和规定。例如，商用飞机的DO-178 C。在这种情况下，软件的成本(例如，每一行代码)要比通常的电话应用程序高得多，软件开发方法也非常不同(而且更加官僚:您将记录并需要正式接受和测试任何更改，甚至是一行修补程序)。