簡單模型檢查工具

是否有簡單的模型檢查工具？我計劃實現一個模型檢查工具，它將分析一些預定義屬性的代碼。簡單模型檢查工具

2008-10-20 Vinay

我認爲你應該嘗試解釋一下更接近你要找的東西...... – 2008-10-20 16:02:59

我認爲你應該修改你的問題，以便它更清楚。這個問題可能涉及十幾種不同的模型檢查場景。 – 2008-10-20 16:04:06

一個重要的工具是SPIN，與Promela語言。如果您使用LaTeX，也有TLA+。

這些不會分析你的代碼，但會讓你表達你的假設和狀態的模型，然後將分析無效狀態。換句話說，他們會檢測你模型中的問題，而不是模型的實現。

我已經看過Goanna的演示，但我不知道它是否可用（商業或其他）;這具有實際分析源代碼的優點。

只要看看你的問題，並再次在你的問題的意見，這聽起來像你真的應該先閱讀一些文獻。也許，The Spin Model Checker或Specifying Systems（可從Leslie Lamport's website下載）。您需要重構您的問題，以免您嘗試解決暫停問題。

2008-10-21 10:34:49 janm

CBMC是一個簡單的工具，我知道它實際上是在代碼上運行。一般而言，模型檢查是一個經過深入研究的領域，但如同人們已經評論的那樣，這個寬度使得很難用所提供的信息來建議一些東西。有成千上萬的SAT求解器，用於HDL /狀態機驗證的正式工具以及大量的商業靜態源分析器。

無論如何，CBMC是一個很好的工具，但不要拿我的話來說;這項工作背後的主要教員Ed Clarke贏得了今年的圖靈獎;-)

2008-10-20 16:17:03

回答