model-checking

    1熱度

    1回答

    要求在Spin中有多個（或全部）違規痕跡

    是否有可能使用Spin獲取屬性的多個（或全部）違規痕跡？ 舉個例子，我創建了下面的PROMELA型號： byte mutex = 0; active proctype A() { A1: mutex==0; /* Is free? */ A2: mutex++; /* Get mutex */ A3: /* A's critical section */ A4: mutex--; /*
    model-checking spin promela 2016-08-30

    1熱度

    1回答

    使用模型檢查器檢查一個特定跟蹤

    我正在使用LTL爲開放式交互協議定義規則。然後我想檢查特定交互是否遵循規範，或者是否有任何規則被破壞。我的直接方法是使用NuSMV，但問題是我沒有我想要檢查的交互模型，但只有一個特定的有限痕跡（所有狀態中的所有變量的值）。 有沒有什麼方法可以在NuSMV中指定？我基本上想輸入NuSMV輸出的模型之一作爲反例： -> State: 1.1 <- a = TRUE b = FALSE -> St
    logic formal-verification model-checking nusmv 2016-09-19

    1熱度

    2回答

    SPIN：解釋錯誤跟蹤

    我試圖解決與農民，狼，山羊和捲心菜有關的任務。 所以，我發現瞭如下因素PROMELA描述： #define fin (all_right_side == true) #define wg (g_and_w == false) #define gc (g_and_c == false) ltl ltl_0 { <> fin && [] (wg && gc) } bool all_righ
    verification model-checking spin promela 2017-01-03

    2熱度

    2回答

    如何用CUDD包替換BDD中的一些變量？

    假設DdManager有四個變量：x, y, x', y'，我有一個由x和y構建的BDD。 現在我想將x更改爲x',y至y'，即得到由x'和y'構建的完全相同的BDD。 如何使用CUDD軟件包得到此結果？我想要實現模型檢查算法時遇到此問題。我想知道如何實現這個操作，或者我是否誤解了符號模型檢查算法？ 非常感謝！
    model-checking binary-decision-diagram cudd 2017-02-24

    1熱度

    1回答

    在NuSMV中構建UART的正式模型？

    我正在學習模型檢查和NuSMV爲我的教育。我可以編輯和運行NuSMV代碼，並且對UART的功能和功能有一個公正的理解。 我的任務是使用NuSMV正式模擬UART，但此時我不知道該怎麼做。我明白，UART傳輸一個字節爲八個連續的位，但我怎樣才能建模？ 我有一個互斥代碼爲出發點： >NuSMV.exe mutex.smv *** This is NuSMV 2.6.0 (compiled on We
    uart formal-verification model-checking nusmv 2017-02-26

    1熱度

    1回答

    將SystemVerilog聲明延遲轉換爲invarspec

    我想將延遲的SystemVerilog聲明轉換爲正式驗證者的invarspec。合成器在下面的代碼行中給出## 1的語法錯誤。 assert property ((req1 == 0) ##1(req1 == 1) ##1 !(req2 == 1) || (gnt1 == 0)); 有幾個屬性需要驗證並有延遲。我目前正在嘗試使用合成器將它們轉換爲正式（SMV）模型規範，該合成器適用於不涉及延遲
    delay formal-verification model-checking system-verilog-assertions 2016-11-22

    1熱度

    1回答

    與LTL公式

    考慮找到一個變量的所有可能的執行最小值操縱共享變量N兩個過程以下Promela型號： byte N = 0; active [2] proctype P(){ byte temp, i; i = 1; do :: i < 10 -> temp = N; temp++; N = temp; i++;
    model-checking promela spin 2016-11-25

    0熱度

    1回答

    系統包含死鎖 - 如何找到它？ （UPPAAL）

    我使用UPPAAL建立了模型，並使用驗證程序檢查死鎖。答案是：財產不滿意。因此存在僵局。 UPPAAL有辦法報告有關死鎖的更多詳細信息，例如特定情況下所有變量的狀態和當前值嗎？
    deadlock model-checking uppaal 2016-11-27

    2熱度

    1回答

    自旋驗證，驗證變量達到一定的數值​​

    這是我在Stack Exchange上的第一個問題，所以如果有任何違規指標，請告訴我。 我有一個用Promela編寫的大學OS和併發系統課程。有兩個進程正在運行，增加一個變量n。我們的任務是編寫這些流程，然後使用Spin中的驗證工具來證明n有可能獲得值4.我已經通讀了所有的命令行參數，但是沒有任何結果對我來說，「插入這個修飾符後跟一個變量名來檢查所有可能的值。」 byte n; proctyp
    concurrency verification model-checking spin promela 2017-03-08

    2熱度

    2回答

    符號執行和模型檢查

    符號執行和模型檢查（例如在模型轉換中）有什麼區別？我不明白他們的區別。他們是一樣的嗎？！
    validation verification model-checking model-driven 2016-08-23
最新問題