1

以下属性对于 check_property 是正确的，但 msat_check_ltlspec_bmc 给出了反例。后一个的结果似乎是正确的。“G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN 模块”。我们如何解释这一点？

我用稍微改变的 smv 文件尝试了这个。试图检查基于 LTL 属性的存在模式。Check_fsm 结果未早先运行。这造成了僵局。在这种情况下 msat_check.... 结果似乎不正确。现在哪一个是正确的？验证模型的正确方法应该是什么？需要使用实数，因此尝试 msat 命令。

MODULE Seq_19(T_41, T_41_PRESENT)
    VAR
        _next_t : { Init_46_idle, LO_51_idle, BO_73_idle, State_120_idle, TO_132_idle, LOSense_118, BOSense_115, TOSense_137, TransitionSegment_125, BOSense_141 };
        FlagLO : boolean;
        FlagBO : boolean;
        tt : -256..255;
        FlagTO : boolean;

    DEFINE
        LOOut_68 := 
            case
                (_next_t = LOSense_118) : TRUE;
                TRUE : FALSE;
            esac;
        BOOut_84 := 
            case
                (_next_t = BOSense_115) : TRUE;
                (_next_t = BOSense_141) : TRUE;
                TRUE : FALSE;
            esac;
        LOOut_68_PRESENT := 
            case
                (_next_t = LOSense_118) : TRUE;
                TRUE : FALSE;
            esac;
        BOOut_84_PRESENT := 
            case
                (_next_t = BOSense_115) : TRUE;
                (_next_t = BOSense_141) : TRUE;
                TRUE : FALSE;
            esac;
        guard_LOSense_118 := (tt > 5);
        guard_BOSense_115 := (tt > 10);
        guard_TOSense_137 := (tt > 8);
        guard_TransitionSegment_125 := (tt > 50);
        guard_BOSense_141 := (tt > 10);

    ASSIGN
        init(_next_t) := { Init_46_idle, LOSense_118 };
        init(FlagLO) := FALSE;
        init(FlagBO) := FALSE;
        init(tt) := 0;
        init(FlagTO) := FALSE;

    TRANS _next_t in { Init_46_idle }
         -> next(_next_t) in { Init_46_idle, LOSense_118 };
    TRANS _next_t in { LO_51_idle, LOSense_118 }
         -> next(_next_t) in { LO_51_idle, BOSense_115, TOSense_137 };
    TRANS _next_t in { BO_73_idle, BOSense_115, BOSense_141 }
         -> next(_next_t) in { BO_73_idle, TransitionSegment_125 };
    TRANS _next_t in { State_120_idle, TransitionSegment_125 }
         -> next(_next_t) in { State_120_idle };
    TRANS _next_t in { TO_132_idle, TOSense_137 }
         -> next(_next_t) in { TO_132_idle, BOSense_141 };
    TRANS (_next_t = Init_46_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = LO_51_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = BO_73_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = State_120_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = TO_132_idle)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = LOSense_118)
         -> next(FlagLO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = BOSense_115)
         -> next(FlagBO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = TOSense_137)
         -> next(FlagTO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO;
    TRANS (_next_t = TransitionSegment_125)
         -> next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagBO) = FlagBO &
            next(FlagTO) = FlagTO;
    TRANS (_next_t = BOSense_141)
         -> next(FlagBO) = TRUE &
            next(tt) = (tt + 1) &
            next(FlagLO) = FlagLO &
            next(FlagTO) = FlagTO;

    INVAR ((_next_t = LOSense_118) -> guard_LOSense_118)
    INVAR ((_next_t = BOSense_115) -> guard_BOSense_115)
    INVAR ((_next_t = TOSense_137) -> guard_TOSense_137)
    INVAR ((_next_t = TransitionSegment_125) -> guard_TransitionSegment_125)
    INVAR ((_next_t = BOSense_141) -> guard_BOSense_141)
    INVAR ((_next_t = Init_46_idle) -> !(guard_LOSense_118))
    INVAR ((_next_t = LO_51_idle) -> (!(guard_BOSense_115) & !(guard_TOSense_137)))
    INVAR ((_next_t = BO_73_idle) -> !(guard_TransitionSegment_125))
    INVAR ((_next_t = State_120_idle) -> TRUE)
    INVAR ((_next_t = TO_132_idle) -> !(guard_BOSense_141))

MODULE main
    VAR
        T_41 : -256..255;
        T_41_PRESENT : boolean;
        module : Seq_19(T_41,T_41_PRESENT);

这是的输出msat_check_ltlspec_bmc：

nuXmv > read_model -i Seq.smv
nuXmv > go_msat
nuXmv > msat_check_ltlspec_bmc -p "G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module"
-- no counterexample found with bound 0
-- no counterexample found with bound 1
-- no counterexample found with bound 2
-- no counterexample found with bound 3
-- no counterexample found with bound 4
-- no counterexample found with bound 5
-- no counterexample found with bound 6
-- specification  G (tt >= 7 ->  G FlagLO = FALSE) IN module is false
-- as demonstrated by the following execution sequence
Trace Description: MSAT BMC counterexample
Trace Type: Counterexample
  -> State: 1.1 <-
    T_41 = -256
    T_41_PRESENT = FALSE
    module._next_t = Init_46_idle
    module.FlagLO = FALSE
    module.FlagBO = FALSE
    module.tt = 0
    module.FlagTO = FALSE
    module.guard_BOSense_141 = FALSE
    module.guard_TransitionSegment_125 = FALSE
    module.guard_TOSense_137 = FALSE
    module.guard_BOSense_115 = FALSE
    module.guard_LOSense_118 = FALSE
    module.BOOut_84_PRESENT = FALSE
    module.LOOut_68_PRESENT = FALSE
    module.BOOut_84 = FALSE
    module.LOOut_68 = FALSE
  -> State: 1.2 <-
    T_41 = 255
    T_41_PRESENT = TRUE
    module.tt = 1
  -> State: 1.3 <-
    T_41 = -238
    T_41_PRESENT = FALSE
    module.tt = 2
  -> State: 1.4 <-
    T_41 = 255
    T_41_PRESENT = TRUE
    module.tt = 3
  -> State: 1.5 <-
    T_41 = -224
    T_41_PRESENT = FALSE
    module.tt = 4
  -> State: 1.6 <-
    T_41 = 255
    T_41_PRESENT = TRUE
    module.tt = 5
  -> State: 1.7 <-
    module._next_t = LOSense_118
    module.tt = 6
    module.guard_LOSense_118 = TRUE
    module.LOOut_68_PRESENT = TRUE
    module.LOOut_68 = TRUE
  -> State: 1.8 <-
    module._next_t = LO_51_idle
    module.FlagLO = TRUE
    module.tt = 7
    module.LOOut_68_PRESENT = FALSE
    module.LOOut_68 = FALSE

这是正常 LTLcheck_property调用的输出：

nuXmv > go
nuXmv > check_property -l -p "G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module"
-- specification  G (tt >= 7 ->  G FlagLO = FALSE) IN module is true

这是的输出check_fsm：

nuXmv > check_fsm

********   WARNING   ********
Fair states set of the finite state machine is empty.
This might make results of model checking not trustable.
******** END WARNING ********

##########################################################
The transition relation is not total. A state without
successors is:
T_41 = -256
T_41_PRESENT = FALSE
module._next_t = State_120_idle
module.FlagLO = FALSE
module.FlagBO = FALSE
module.tt = 255
module.FlagTO = FALSE
The transition relation is not deadlock-free.
A deadlock state is:
T_41 = -256
T_41_PRESENT = FALSE
module._next_t = State_120_idle
module.FlagLO = TRUE
module.FlagBO = TRUE
module.tt = 255
module.FlagTO = TRUE
##########################################################
4

1 回答 1

1

的输出check_fsm告诉您问题出在哪里：FSM中存在死锁状态。

请参阅常见问题解答 #011

在 NuSMV 中实现的基于 BDD 的 LTL 模型检查算法仅与无限路径有关。因此，即使对于不成立的安全属性，也会生成套索形状的反例，尽管有限路径就足够了。在进行检查时，假设转移关系的整体性和不存在死锁，并且搜索仅限于考虑无限路径，而忽略导致死锁的所有路径。因此，将不会检测到导致死锁和伪造属性的有限路径。

基于 SAT 的有界模型检查算法还假设转移关系的整体性和不存在死锁，但他们正在为给定的有限或无限属性寻找反例。因此，与基于 BDD 的 LTL 模型检查算法不同，将检测到导致死锁和伪造属性的有限路径。

两种算法都假设转移关系的整体性和不存在死锁，但它们没有专门检查是否满足这些条件。用户有责任通过例如在批处理模式下发出 -ctt 命令行标志或通过在 NuSMV shell 中调用 check_fsm 命令来执行此检查。

到目前为止，还没有标志可以禁用在基于 SAT 的有界模型检查中搜索有限路径。但是，通过在模型中添加以下正义公平条件

正义真实；

有界模型检查算法停止寻找有限路径并将搜索限制为仅无限路径：

当 NuSMV 模型包含多个初始状态时，报告的验证结果可能会发生差异。基于 BDD 的方法依赖于将 LTL 模型检查减少到 CTL 模型检查（通过画面构造）。CTL 模型检查普遍量化了一组公平的初始状态。因此，仅考虑公平的初始状态。可能存在不公平的初始状态，它们不被考虑。这种选择可能是有问题的，但 CadenceSMV 也显示了这一点。不同的是，基于 BMC 的模型检查并不局限于只考虑公平的初始状态。因此，如果存在一个不公平的初始状态，并且从中存在一条有限路径，它将违反公平条件。

于 2019-01-13T05:33:52.260 回答