model-checking

5熱度

3回答

模型檢查大型分佈式C++項目（如KDE）的工具？

是否有一種工具可以處理模型檢查大型的現實世界中大多數爲C++的分佈式系統，比如KDE？ （KDE是一個使用IPC的分佈式系統，儘管通常所有進程都在同一臺機器上。順便提一句，這是「分佈式系統」的有效用法 - 檢查維基百科。 ） 該工具需要能夠處理內部進程事件和進程間消息。 （讓我們假設，如果該工具支持C++，但不支持KDE使用諸如MOC其他的東西，我們能砍東西一起要解決這一點。） 我會很樂意接受少將

c++ static-analysis formal-methods formal-verification model-checking 2010-11-10

---

2熱度

1回答

如何獲取UPPAAL中的時鐘當前值並將其存儲在整型變量中？

任何人都可以告訴我如何獲取時鐘變量的當前值並存儲在整數變量中。我試過k = t（其中k是整數，t是時鐘），但它會拋出「不兼容的類型錯誤」。我也嘗試過k =（int）t，但它引發了「意外的T_INT」語法錯誤。 是否有任何類型轉換可用於UPPAAL中的時鐘以獲取時鐘的當前值並將其存儲在變量中？

model-checking 2011-11-11

---

1熱度

1回答

從Spin Modelchecker瞭解錯誤路徑

我試圖使用自旋模型檢查器來模擬兩個對象（A和B）之間的遊戲。物體在板上移動，每個位置由其（x，y）座標定義。這兩個物體應該不會相撞。我有三個進程：init，A Model，B Model。我的模型檢驗的LTL性質：（活躍度屬性來檢查，如果兩個物體永遠佔據相同的位置） ltl prop1 { [] (!(x_a == x_b) && !(y_a == y_b)) } 錯誤線索，我得到的是： 初始

model-checking spin 2012-04-13

---

4熱度

1回答

自旋 - 形式化驗證

有沒有人有這個工具SPIN，甚至更多的model checking（併發程序）的任何信息

model-checking spin 2011-05-17

---