単純なモデルチェッカーツール

Question

単純なモデルチェッカーツールはありますか。事前定義されたプロパティのコードを分析するモデルチェッカーツールを実装する予定です。

Answer 1

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

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

Goanna のデモを見ましたが、見ていませんt（商用またはその他）が利用可能かどうかを知る。これには、ソースコードを実際に分析するという利点があります。

質問と質問のコメントをもう一度見ると、最初にいくつかの文献を読む必要があるようです。おそらく、スピンモデルチェッカー、または指定システム（ Leslie LamportのWebサイト）。停止する問題を解決しようとしないように、問題を再構成する必要があります。

Answer 2

CBMC は、私が知っているシンプルなツールの1つです。実際にコードを操作します。一般にモデル検査は非常に研究されている分野ですが、人々がすでにコメントしているように、この幅は提供された情報で何かを提案することを困難にします。数千のSATソルバー、HDL /ステートマシン検証用の公式ツール、および多数の市販の静的ソースアナライザーがあります。

いずれにせよ、CBMCは優れたツールですが、私の言葉を受け入れないでください。この作品の主な教職員であるエド・クラークは、今年チューリング賞を受賞しました;-）