5

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

（KDE 在使用 IPC 的意义上是一个分布式系统，尽管通常所有进程都在同一台机器上。是的，顺便说一句，这是“分布式系统”的有效用法 - 检查 Wikipedia。）

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

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

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

4

3 回答 3

6

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

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

一个重要的问题是每个人对他们想要检查的模型有不同的想法。仅此一项就可能会扼杀您准确找到您想要的东西的机会，因为每个模型提取工具通常都会选择它想要捕获的模型，并且它与您想要的精确匹配的机会恕我直言接近于零。

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

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

这篇论文声称可以做到这一点，但我没有详细研究：Compositional analysis of C/C++programs with VeriSoft。相关的是[PDF] VeriSoft 的计算机辅助假设/保证推理。看来您必须手动注释源代码以指示感兴趣的建模元素。Verifysoft 工具本身似乎是贝尔实验室专有的，可能很难获得。

与此类似： 多线程 C++ 程序的分布式验证。

这篇论文也提出了一些有趣的主张，但没有处理 C++，尽管标题是： 多线程 C/C++ 程序的运行时模型检查。

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

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

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

于 2010-11-10T11:18:13.193 回答
1

第一次使用静态代码分析器处理大型代码库时，通常会产生如此多的警告和警报，以至于您无法在合理的时间内分析所有这些。很难从对工具来说看起来很可疑的代码中找出真正的问题。

您可以尝试使用自动不变量发现工具，如“Daikon”，在运行时捕获感知的不变量。您可以稍后验证发现的不变量（例如变量“a == b+1”的等价性）是否有意义，然后将永久断言插入到您的代码中。这样，当您的更改导致不变量被违反时，您将收到警告，提示您可能因更改而破坏了某些东西。此方法有助于避免重组或更改代码以添加测试和模拟。

于 2010-12-17T06:51:53.067 回答
0

将形式化技术应用于大型系统的通常方法是将它们模块化并为每个模块的接口编写规范。然后您可以独立地验证每个模块（在验证模块时，您导入它调用的其他模块的规范 - 但不是代码）。这种方法使验证具有可扩展性。

于 2011-02-10T01:45:17.527 回答