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

Formal methods in C++ for safety critical software

本文关键字：c++ 形式化方法软件安全更新时间：2023-10-16

看看C, C对可以在代码中使用的形式方法(frame - C, VCC, verifast)有很好的支持。据我所知，c++似乎没有任何可与之相比的。

对于用c++编写的安全关键软件的推理，有哪些形式化的方法可用?

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

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

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

注意Klocwork有一个MISRA c++的扩展。

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