是否有一个工具可以处理模型检查大型，真实世界，主要是C ++，分布式系统，如KDE？
（KDE是一个分布式系统，因为它使用IPC，虽然通常所有进程都在同一台机器上。顺便说一下，这是“分布式系统”的有效用法 - 检查维基百科。）
该工具需要能够处理进程内事件和进程间消息。
（假设如果该工具支持C ++，但不支持KDE使用的其他东西，如moc，我们可以一起破解某些东西以解决这个问题。）
我很乐意接受不太通用的（例如专门用于查找特定类型的错误的静态分析器）或更一般的静态分析替代方案，而不是实际的模型检查器。但我只对能够实际处理KDE大小和复杂性项目的工具感兴趣。
您显然正在寻找可以的静态分析工具
一个重要的问题是，每个人对于他们想要检查的模型有不同的看法。仅这一点可能会让你有机会找到你想要的东西，因为每个模型提取工具通常都会选择它想要捕获的模型，并且它与你想要的精确匹配的机会是IMHO接近于零。
你不清楚你想要建模的具体内容，但我认为你想要找到通信原语并建模过程交互以检查死锁之类的东西？
商业静态分析工具供应商看起来似乎是一个合乎逻辑的地方，但我认为它们并不存在。 Coverity似乎是最好的选择，但似乎他们只对Java线程问题进行了某种动态分析。
本文声称这样做，但我没有详细研究过：Compositional analysis of C/C++ programs with VeriSoft。相关的是[PDF] Computer-Assisted Assume/Guarantee Reasoning with VeriSoft。您似乎必须手动注释源代码以指示感兴趣的建模元素。 Verifysoft工具本身似乎是贝尔实验室专有的，可能很难获得。
同样这一个：Distributed Verification of Multi-threaded C++ Programs 。
本文也提出了有趣的说法，但尽管标题为：Runtime Model Checking of Multithreaded C/C++ Programs，但它并没有处理C ++。
虽然这很困难，但他们共同的一个问题是解析C ++（如前面引用的论文所示）并找到提供模型原始信息的代码模式。您还需要解析您正在使用的C ++的特定方言; C ++编译器都接受不同的语言并不好。而且，正如您所观察到的，处理大型C ++代码是必要的。模型检查器（SPIN和朋友）相对容易找到。
我们的DMS Software Reengineering Toolkit提供了通用的解析，可定制的模式匹配和事实提取，并且具有强大的C++ Front End，可处理许多C ++方言（编辑2019年2月：包括Ansi中的C ++ 17，GCC和MS风格）。它可能被配置为查找和提取与您关注的模型相对应的事实。但是这不是现成的。
具有C前端的DMS已被用于处理极大的C应用程序（19,000个编译单元！）。 C ++前端已被广泛用于各种大型C ++项目（EDIT 2019年2月：包括跨3000多个编译单元的API的大规模重构）。鉴于DMS的一般功能，我认为它可能能够处理相当大的代码块。因人而异。
静态代码分析器在第一次用于大型代码库时通常会产生如此多的警告和警报，导致您无法在合理的时间内分析所有这些警报和警报。从看起来可疑的代码到工具中挑出真正的问题是很困难的。
您可以尝试使用自动不变的发现工具，如“Daikon”，在运行时捕获感知的不变量。您可以稍后验证发现的不变量（例如变量的等效性“a == b + 1”）是否有意义，然后将永久断言插入到代码中。这种方式当你因为你的改变而违反了不变量时，你会得到一个警告，也许你可能因为你的改变而破坏了某些东西。此方法有助于避免重构或更改代码以添加测试和模拟。
将正式技术应用于大型系统的通常方法是将它们模块化并为每个模块的接口编写规范。然后，您可以独立验证每个模块（在验证模块时，您导入其调用的其他模块的规范 - 但不是代码）。这种方法使得验证可扩展。