使用模型检查器检查一个特定的轨迹

Question

我正在使用 LTL 来定义开放交互协议的规则。然后我想检查特定的交互是否遵循规范，或者是否违反了任何规则。我的直接方法是使用 NuSMV，但问题是我没有要检查的交互模型，只有一个特定的有限轨迹（所有状态下所有变量的值）。

有什么方法可以在 NuSMV 中指定它吗？我基本上想输入 NuSMV 输出的模型之一作为反例：

-> State: 1.1 <-
a = TRUE
b = FALSE
-> State: 1.2 <-
a = FALSE
-> State: 1.3 <-
a = TRUE

并验证。或者 NuSMV 是错误的工具吗？

谢谢！

Answer 1

经过一番思考，我找到了在 NuSMV 模型中对特定轨迹进行编码的解决方案。这很简单，诀窍是为轨迹的每个状态使用一个变量。

例如，我想对交互进行编码，并且我只希望在每个状态下最后说出的消息都是真实的。如果要编码的交互是 ['a'、'b'、'a']，则 NuSMV 模型将是：

MODULE main
VAR
a : boolean;
b : boolean;
state : {s0,s1,s2};

ASSIGN
init(a) := FALSE;
init(state) := s0;
next(a) := 
    case
        state = s0 : TRUE;
        state = s1 : FALSE;
        state = s2 : TRUE;
    esac;
next(b) := 
    case
        state = s0 : FALSE;
        state = s1 : TRUE;
        state = s2 : FALSE;
    esac;
next(state) := 
    case
        state = s0 : s1;
        state = s1 : s2;
        state = s2 : s2;
    esac;

我希望它可能对某人有用！

使用模型检查器检查一个特定的轨迹

Use model checker to check one particular trace

logic

model-checking

formal-verification

nusmv