是否有一種工具可以處理模型檢查大型的現實世界中大多數爲C++的分佈式系統，比如KDE？ （KDE是一個使用IPC的分佈式系統，儘管通常所有進程都在同一臺機器上。順便提一句，這是「分佈式系統」的有效用法 - 檢查維基百科。 ）模型檢查大型分佈式C++項目（如KDE）的工具？
該工具需要能夠處理內部進程事件和進程間消息。
（讓我們假設，如果該工具支持C++，但不支持KDE使用諸如MOC其他的東西，我們能砍東西一起要解決這一點。）
我會很樂意接受少將軍（如專門用於查找特定類別的錯誤的靜態分析器）或更一般的靜態分析替代方案，以代替實際的模型檢查器。但我只對實際上處理KDE大小和複雜性的工具感興趣。
你顯然在尋找一個靜態分析工具，可以對大規模
一個重要的問題是，每個人對於他們想要檢查的模型都有不同的想法。 這可能會殺死你找到你想要的東西的機會，因爲每個模型提取工具 一般都會選擇它作爲模型捕獲什麼，以及它匹配的機會 你想要的就是IMHO close歸零。
你不清楚你想要建模什麼，但我想你想找到通信 基元和模型的過程相互作用來檢查像死鎖？
商業靜態分析工具供應商似乎是一個合乎邏輯的地方看，但我不認爲他們在那裏。 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。
本文也使有趣的聲明，但不處理C++，儘管標題： Runtime Model Checking of Multithreaded C/C++ Programs。儘管所有這些部分都很困難，但他們都共享的一個問題是解析C++（例如前面引用的論文中的 ），並找到爲模型提供原始信息的代碼模式。 您還需要解析您正在使用的C++的特定方言;它不是很好，C++編譯器都接受不同的語言。而且，正如您所觀察到的，處理大型C++代碼是必要的。模型跳棋（SPIN和朋友）相對容易找到。
我們的DMS Software Reengineering Toolkit提供了通用的解析，可定製的模式匹配和事實抽取，並且有一個強大的C++ Front End，可處理C++的許多方言。它可能被配置爲查找和提取與您關心的模型相對應的事實。但是這並不是現成的。
DMS及其前端C已用於處理超大型C應用程序（19,000個編譯單元！）。 C++前端已經在各種大型C++項目中被憤怒地使用，但通常不是那種規模。鑑於DMS的一般功能，我認爲它可能能夠處理相當大的代碼塊。因人而異。
靜態代碼分析器在首次針對大型代碼庫使用時，通常會產生如此多的警告和警報，以至於無法在合理的時間內分析所有這些警告和警報。很難從代碼中挑出真正的問題，這些代碼只是看起來對工具可疑。
您可以嘗試使用自動不變的發現工具，如「Daikon」，可在運行時捕獲感知的不變量。如果發現的不變量（例如變量「a == b + 1」的等價性）有意義，然後將永久斷言插入代碼中，您可以稍後進行驗證。通過這種方式，當您的更改導致不變時，您會收到一條警告，說明您的更改可能會導致某些問題。此方法有助於避免重構或更改代碼以添加測試和模擬。
將正式技術應用於大型系統的常用方法是將它們模塊化，併爲每個模塊的接口編寫規範。然後，您可以獨立驗證每個模塊（在驗證模塊時，您導入其調用的其他模塊的規範（而不是代碼））。這種方法使驗證可擴展。
作爲對問題的評論而不是答案，這會更好。我明白這是一種方法，但它實際上是一種昂貴的方法，而且它無法回答具體的問題：哪種工具適合這種現實世界的使用？ – 2011-02-12 09:38:58
是否有大*非真實世界主要是C++分佈式系統？ :-) – Ken 2010-11-10 06:54:25
你能澄清你的意思是模型檢查嗎？ – 2010-11-10 06:54:26
我確定他意味着狀態空間檢查屬性（http://en.wikipedia.org/wiki/Model_checking的一些特定實例），並且他告訴我們他有一個使用消息傳遞的分佈式系統給了我們一個提示基元，所以存在由過程交互形成的一組隱含狀態。但細節很重要。 – 2010-11-10 11:21:41