c++ - 安全关键软件的 C++ 形式化方法

Question

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

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

Answer 1

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

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

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

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

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