5

KDE などの大規模で実世界のほとんどが C++ の分散システムのモデル チェックを処理できるツールはありますか?

(KDE は IPC を使用するという意味で分散システムですが、通常はすべてのプロセスが同じマシン上にあります。はい、ちなみに、これは「分散システム」の有効な使用法です - ウィキペディアを確認してください。)

このツールは、プロセス内イベントとプロセス間メッセージを処理できる必要があります。

(ツールが C++ をサポートしているが、moc などの KDE が使用する他のものをサポートしていない場合、何かをハックして回避できると仮定しましょう。)

実際のモデル チェッカーの代わりに、あまり一般的でないもの (特定のクラスのバグを見つけることに特化した静的アナライザーなど) またはより一般的な静的解析の代替手段を喜んで受け入れます。しかし、私が興味を持っているのは、KDE ​​の規模と複雑さのプロジェクトを実際に処理できるツールだけです。

4

3 に答える 3

6

あなたは明らかに、できる静的分析ツールを探しています

  • C++ を大規模に解析する
  • 関心のあるコードフラグメントを見つける
  • モデルを抽出する
  • そのモデルをモデル チェッカーに渡す
  • その結果をあなたに報告する

重大な問題は、どのモデルをチェックしたいかについて、誰もが異なる考えを持っていることです。各モデル抽出ツールは通常、モデルとしてキャプチャしたいものを選択しており、必要なものと正確に一致する可能性はゼロに近いため、それだけでは、必要なものを正確に見つけるチャンスが失われる可能性があります.

具体的に何をモデル化したいのか明確ではありませんが、通信プリミティブを見つけてプロセスの相互作用をモデル化し、デッドロックのようなものをチェックしたいと思いますか?

商用の静的解析ツールのベンダーは一見当然のことのように思えますが、まだそこにはいないと思います。 Coverityが最善の策のように思えますが、Java スレッドの問題について何らかの動的分析しかできないようです。

この論文ではこれを行うと主張していますが、詳しくは調べていません。VeriSoft を使用した C/C++ プログラムの構成分析 関連は[PDF] Computer-Assisted Assume/Guarantee Reasoning with VeriSoftです。関心のあるモデリング要素を示すために、ソース コードに手動で注釈を付ける必要があるようです。Verifysoft ツール自体は、Bell Labs 独自のようであり、入手が難しい可能性があります。

同様に、これ はマルチスレッド C++ プログラムの分散検証です。

この論文も興味深い主張をしていますが、タイトルが「 Runtime Model Checking of Multithreaded C/C++ Programs」であるにもかかわらず、C++ を処理していません 。

これのすべての部分は困難ですが、すべてに共通する問題は、C++ を解析し (前に引用した論文で例示されているように)、モデルの生の情報を提供するコード パターンを見つけることです。また、使用している C++ の特定の方言を解析する必要があります。C++ コンパイラがすべて異なる言語を受け入れるのは良くありません。そして、ご覧のとおり、大きな C++ コードの処理が必要です。モデル チェッカー (SPIN など) は比較的簡単に見つかります。

当社のDMS ソフトウェア リエンジニアリング ツールキットは、カスタマイズ可能なパターン マッチングとファクト抽出を備えた汎用解析を提供し、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 に答える