Rob*_*een 5 c++ model-checking formal-verification formal-methods static-analysis
是否有一个工具可以处理模型检查大型,真实世界,主要是C++,分布式系统,如KDE？
(KDE是一个分布式系统,因为它使用IPC,虽然通常所有进程都在同一台机器上.顺便说一下,这是"分布式系统"的有效用法 - 检查维基百科.)
该工具需要能够处理进程内事件和进程间消息.
(假设如果该工具支持C++,但不支持KDE使用的其他东西,如moc,我们可以一起破解某些东西以解决这个问题.)
我很乐意接受不太通用(例如专门用于查找特定类型的错误的静态分析器)或更一般的静态分析替代方案,而不是实际的模型检查器.但我只对能够实际处理KDE大小和复杂性项目的工具感兴趣.
您显然正在寻找可以的静态分析工具
一个重要的问题是,每个人对于他们想要检查的模型有不同的看法.仅这一点可能会让你有机会找到你想要的东西,因为每个模型提取工具通常都会选择它想要捕获的模型,并且它与你想要的精确匹配的机会是IMHO接近于零.
你不清楚你想要建模的具体内容,但我认为你想要找到通信原语并建模过程交互以检查死锁之类的东西？
商业静态分析工具供应商看起来似乎是一个合乎逻辑的地方,但我认为它们并不存在. Coverity似乎是最好的选择,但似乎他们只对Java线程问题进行了某种动态分析.
本文声称这样做,但我没有详细研究过:使用VeriSoft对C/C++程序进行成分分析.相关的是使用VeriSoft的[PDF]计算机辅助假设/保证推理.您似乎必须手动注释源代码以指示感兴趣的建模元素.Verifysoft工具本身似乎是贝尔实验室专有的,可能很难获得.
类似这一个: 多线程C++程序的分布式验证.
本文也提出了有趣的说法,但不管标题如何处理C++: 多线程C/C++程序的运行时模型检查.
虽然这很困难,但他们共同的一个问题是解析C++(如前面引用的论文所示)并找到提供模型原始信息的代码模式.您还需要解析您正在使用的C++的特定方言; C++编译器都接受不同的语言并不好.而且,正如您所观察到的,处理大型C++代码是必要的.模型检查器(SPIN和朋友)相对容易找到.
我们的DMS软件再造工具包提供通用解析,可定制的模式匹配和事实提取,并具有强大的C++前端,可处理许多C++方言.它可能被配置为查找和提取与您关注的模型相对应的事实.但是这不是现成的.
具有C前端的DMS 已被用于处理极大的C应用程序(19,000个编译单元!).C++前端已被用于各种大型C++项目的愤怒,但通常不是那种规模.鉴于DMS的一般功能,我认为它可能能够处理相当大的代码块.因人而异.