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

我正在學習模型檢查和NuSMV爲我的教育。我可以編輯和運行NuSMV代碼，並且對UART的功能和功能有一個公正的理解。在NuSMV中構建UART的正式模型？

我的任務是使用NuSMV正式模擬UART，但此時我不知道該怎麼做。我明白，UART傳輸一個字節爲八個連續的位，但我怎樣才能建模？

我有一個互斥代碼爲出發點：

>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))

來源

2017-02-26 Niklas Rosencrantz