c++ - 用于模型检查大型分布式 C++ 项目(如 KDE)的工具？

Question

是否有一种工具可以处理大型、真实世界、主要是 C++ 分布式系统(例如 KDE)的模型检查？

(KDE 在使用 IPC 的意义上是一个分布式系统，尽管通常所有进程都在同一台机器上。是的，顺便说一下，这是“分布式系统”的有效用法 - 查看维基百科。)

该工具需要能够处理进程内事件和进程间消息。

(假设该工具支持 C++，但不支持 KDE 使用的其他东西，例如 moc，我们可以一起破解一些东西来解决这个问题。)

我很乐意接受不太通用的(例如，专门用于查找特定错误类别的静态分析器)或更通用的静态分析替代方案，以代替实际的模型检查器。但我只对能够实际处理 KDE 规模和复杂性项目的工具感兴趣。

Answer 1

您显然正在寻找一种静态分析工具，它可以

• 大规模解析 C++
• 找到感兴趣的代码片段
• 提取模型
• 将该模型传递给模型检查器
• 向您报告该结果

一个重要的问题是每个人对于他们想要检查的模型都有不同的想法。仅此一项就可能会扼杀您准确找到所需内容的机会，因为每个模型提取工具通常已经选择了它想要捕捉什么作为模型，以及它匹配的机会你想要的恰恰是恕我直言接近于零。

您不清楚具体要建模什么，但我想您想要找到沟通方式原语并对流程交互建模以检查死锁之类的东西？

商业静态分析工具供应商似乎是一个合乎逻辑的地方，但我认为他们还没有出现。 Coverity这似乎是最好的选择，但他们似乎只对 Java 线程问题进行了某种动态分析。

本文声称要这样做，但我没有详细查看:Compositional analysis of C/C++ programswith VeriSoft .相关的是[PDF] Computer-Assisted Assume/Guarantee Reasoning with VeriSoft .看来您必须手动注释指示感兴趣的建模元素的源代码。 Verifysoft 工具本身似乎是贝尔实验室的专利，可能很难获得。

与此类似:Distributed Verification of Multi-threaded C++ Programs .

这篇论文也提出了有趣的主张，但尽管标题如此，但并未处理 C++: Runtime Model Checking of Multithreaded C/C++ Programs .

虽然这所有的部分都很困难，但它们共同的一个问题是解析 C++(例如之前引用的论文)并找到为模型提供原始信息的代码模式。您还需要解析您正在使用的 C++ 的特定方言； C++ 编译器都接受不同的语言，这并不好。而且，正如您所观察到的，处理大型 C++ 代码是必要的。模型检查器(SPIN 和 friend )相对容易找到。

我们的 DMS Software Reengineering Toolkit提供通用解析，具有可定制的模式匹配和事实提取，并具有强大的 C++ Front End处理许多 C++ 方言(2019 年 2 月编辑:包括 Ansi、GCC 和 MS 风格的 C++17)。它可能被配置为查找和提取与您关心的模型相对应的事实。但它并不是现成的。

DMS 及其 C 前端已用于处理超大型 C 应用程序(19,000 个编译单元!)。 C++ 前端已被愤怒地用于各种大型 C++ 项目(2019 年 2 月编辑:包括跨 3000 多个编译单元的 API 的大规模重构)。鉴于 DMS 的一般能力，我认为它可能能够处理相当大的代码块。 YMMV.