2

シンプルなモデル チェッカー ツールはありますか。定義済みのプロパティのコードを分析するモデル チェッカー ツールを実装する予定です。

4

2 に答える 2

5

重要なツールの 1 つは、Promela 言語を使用したSPINです。LaTeX を使用する場合は、TLA+もあります。

これらはコードを分析しませんが、仮定と状態遷移のモデルを表現し、無効な状態を分析します。つまり、モデルの実装ではなく、モデルの問題を検出します。

Goannaのデモを見たことがありますが、それが利用可能かどうかはわかりません (商用またはその他)。これには、ソース コードを実際に分析できるという利点があります。

あなたの質問とあなたの質問のコメントをもう一度見ると、最初にいくつかの文献を読む必要があるように思えます. おそらく、The Spin Model Checker、またはSpecifying Systems ( Leslie Lamport の Web サイト からダウンロード可能) です。停止している問題を解決しようとしないように、問題を再構成する必要があります。

于 2008-10-21T10:34:49.117 に答える
2

CBMCは、実際にコード上で動作することを認識しているシンプルなツールの 1 つです。一般的に、モデル チェックは十分に研究されている分野ですが、人々がすでにコメントしているように、この範囲が広いため、提供された情報で何かを提案することは困難です。何千もの SAT ソルバー、HDL/ステート マシン検証用の正式なツール、商用の静的ソース アナライザーが多数あります。

いずれにせよ、CBMC は優れたツールですが、私の言葉を鵜呑みにしないでください。この作品の主要な教員である Ed Clarke は、今年チューリング賞を受賞しました ;-)

于 2008-10-20T16:17:03.873 に答える