自旋 - 形式化驗證

有沒有人有這個工具SPIN，甚至更多的model checking（併發程序）的任何信息自旋 - 形式化驗證

2011-05-17 cMinor

是，SPIN是一個很好的模式檢查，但我不知道你要什麼模型檢驗的接觸？你只是想聽到，是的，我聽說過和玩過SPIN，或者你想要建議如何建模檢查源代碼？

例如，如果你是一個C程序員，讓你的手在ESBMC，寫一個小程序，並在其上運行ESBMC。

這應該讓你開始瞭解什麼可以做，以及如何做到這一點。順便說一下，對於初學者模型檢查不是靜態分析。它實際上更強大。這是反靜態分析。模型檢查實際上'（非常狹義）'模擬你的程序並找到實際上失敗的情況（參數組合，例外情況，邊界情況）。

2011-07-20 16:10:22

Eh？它完全是*靜態分析：它源於源代碼。您可能會認爲它與其他靜態分析儀不同，但我不明白它的用途。他們都是不同的。 – 2011-07-20 16:42:19

對不起，它不是。代碼是動態分析的，因此它不是靜態的。模型檢測器不執行代碼本身，而是生成模擬的模型。因此它不是靜態分析。 lint是一個靜態分析器。 SPIN不是。 – 2011-07-28 08:23:13

我認爲你的定義很混亂。動態分析意味着捕獲*程序*運行的信息。使用SPIN，您可以提取程序的抽象模型（通常使用靜態分析！），然後使用SPIN枚舉狀態空間。狀態空間的模擬與程序執行沒有任何關係。目前沒有「計劃」可以執行。 – 2011-07-28 11:37:36

回答