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
最新问题