1
저는 교육에 대한 모델 검사와 NuSMV를 배우고 있습니다. NuSMV 코드를 편집하고 실행할 수 있으며 UART가 무엇인지에 대해 공정하게 이해하고 있습니다.NuSMV에서 UART의 공식 모델을 구축 하시겠습니까?
내 작업은 공식적으로 NuSMV로 UART를 모델링하는 것이지만 현재로서는 어떻게해야할지 모르겠다. UART가 8 바이트 순차 비트로 1 바이트를 전송한다는 것을 알고 있지만 어떻게 모델링 할 수 있습니까?
나는 출발점으로 뮤텍스 코드가 :
>NuSMV.exe mutex.smv
*** This is NuSMV 2.6.0 (compiled on Wed Oct 14 15:37:51 2015)
*** Enabled addons are: compass
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <[email protected]>.
*** Please report bugs to <Please report bugs to <[email protected]>>
*** Copyright (c) 2010-2014, Fondazione Bruno Kessler
*** This version of NuSMV is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado
*** This version of NuSMV is linked to the MiniSat SAT solver.
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson
-- specification EF (state1 = c1 & state2 = c2) is false
-- as demonstrated by the following execution sequence
Trace Description: CTL Counterexample
Trace Type: Counterexample
-> State: 1.1 <-
state1 = n1
state2 = n2
turn = 1
-- specification AG (state1 = t1 -> AF state1 = c1) is true
-- specification AG (state2 = t2 -> AF state2 = c2) is true
MODULE main
VAR
state1: {n1, t1, c1};
ASSIGN
init(state1) := n1;
next(state1) :=
case
(state1 = n1) & (state2 = t2): t1;
(state1 = n1) & (state2 = n2): t1;
(state1 = n1) & (state2 = c2): t1;
(state1 = t1) & (state2 = n2): c1;
(state1 = t1) & (state2 = t2) & (turn = 1): c1;
(state1 = c1): n1;
TRUE : state1;
esac;
VAR
state2: {n2, t2, c2};
ASSIGN
init(state2) := n2;
next(state2) :=
case
(state2 = n2) & (state1 = t1): t2;
(state2 = n2) & (state1 = n1): t2;
(state2 = n2) & (state1 = c1): t2;
(state2 = t2) & (state1 = n1): c2;
(state2 = t2) & (state1 = t1) & (turn = 2): c2;
(state2 = c2): n2;
TRUE : state2;
esac;
VAR
turn: {1, 2};
ASSIGN
init(turn) := 1;
next(turn) :=
case
(state1 = n1) & (state2 = t2): 2;
(state2 = n2) & (state1 = t1): 1;
TRUE : turn;
esac;
SPEC
EF((state1 = c1) & (state2 = c2))
SPEC
AG((state1 = t1) -> AF (state1 = c1))
SPEC
AG((state2 = t2) -> AF (state2 = c2))