用于安全关键软件的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++的扩展。

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