NuSMVでUARTの正式なモデルを構築しますか？

Question

私は教育のためにモデル検査とNuSMVを学んでいます。私はNuSMVコードを編集して実行することができ、私はUARTが何であるかを公正に理解しています。

私の仕事は、正式にUARTをNuSMVでモデル化することですが、現時点ではどのように行うのかよくわかりません。私は、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 <nusmv-users@list.fbk.eu>. 
*** Please report bugs to <Please report bugs to <nusmv-users@fbk.eu>> 

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

Answer 1

はSMVモデルに飛び込む前に、あなたはあなたが興味のあるディテールのレベルで理解するために必要なコードUARTコンポーネントのモデリング構文上の問題に悩まされないように、最初に異なる形式化でコンポーネントをモデル化すると便利です。コンポーネントの入力は何ですか？出力は何ですか？内部状態はありますか？内部状態は時間とともに、特に1つのステップでどのように変化しますか？

ハードウェア記述言語（VerilogやVHDLなど）に精通している場合は、SMVの移行をクロックティックと見なすことができるため、これは非常に良い出発点になります。これらの言語がわからない場合は、代わりにソフトウェアを書くことができます。これはシステムの入出力を理解するのに役立ちますが、SMVへの変換はそれほど迅速ではありません。

非常にステートフルなコンポーネントの場合、対応するオートマトンを手動で描画すると役立ちます。