安全关键软件的 C++ 形式化方法答案

【问题标题】：Formal methods in C++ for safety critical software安全关键软件的 C++ 形式化方法
【发布时间】：2014-09-14 00:02:14
【问题描述】：

看看 C，C 对可以在代码中使用的形式化方法有很好的支持（frama-c、VCC、verifast）。据我所知，C++ 似乎没有任何可比性。

有哪些形式化方法可用于推理用 C++ 编写的安全关键型软件？

【问题讨论】：

如果您正在编写安全关键型软件，您可能需要遵守一个认证标准和一个需要回答的安全权威。这些明确说明了他们对您的期望。那是C++代码吗？通常，不，尽管总是可以解释为什么你认为它是工作的更好工具。正式的方法？通常，不会再出现，尽管新的 DO-178C 航空标准中有一个附录。什么标准和权威适用于您的案例？
在我们的案例中，我们正在研究 2 类医疗，它不受任何特定编码标准的指导，但确实具有软件流程标准。在 2 类和 3 类设备世界中，Misra 是一个非常安全的编码标准，但也不需要正式的方法。这个问题更多地与我们未来的发展和学习有关，而不是具体的项目。我听说 DO178C 标准有一部分是关于形式化方法的，我订购了一本关于它的书，看看发生了什么。这是一个跟进，看看其他人在 C++ 中使用了什么
您可能需要查看 MISRA C++ 编码指南。有支持该标准的静态分析工具。这些工具还有其他检查器来增强 MISRA 标准检查。
我与 Frama-C 开发团队关系密切，我可以说 C++ 前端正在开发中。这是欧盟项目的一部分，其中 VeriFast 也获得了 C++ 前端，并共享了一些资源。一些信息可在llvm.org/devmtg/2014-04/PDFs/Posters/FramaC.pdf
是的。谢谢帕斯卡！这正是我所希望的。该网站的信息有点稀缺。我可以从论文和演示文稿中看到他们可能已经完成了 WP1 并且处于 WP2 中间的某个位置。我不确定你是否可以说，但对于 alpha 类型的东西何时可能最终可用有任何直觉吗？

标签： c++ c formal-methods safety-critical

【解决方案1】：

与我合作的一家医疗公司使用Coverity 和Klocwork 检查代码中可能存在的问题，例如资源泄漏和未初始化的指针被使用。

但是，这些是工具，而不是安全关键代码的标准。

我所看到的是 MISRA 一直在为 C++ 制定标准。他们从 C 开始，大约 5 年前开始研究 C++。例如，一个大问题是 C++ 的 MISRA 标准规定您不应该使用模板。这确实限制了您在 C++ 中可以做的事情。但是，您可以使用该文档作为起点。例如，您可能希望将软件中使用的模板限制为标准库和 boost 中的模板。

请注意，Klocwork 具有MISRA C++ 的扩展名。

然而，编写好代码的最佳方法之一是使用单元测试和集成测试对其进行测试。多年来我发现这比大多数其他方法更可靠。

【讨论】：

Formal methods 与 MISRA 无关。 MISRA 只是一种用于将编程语言简化为安全子集的编码标准。如果您正在查看更核心的、特定于应用程序的安全标准，它们将要求您同时使用形式化方法和编程语言的安全子集。