NuSMV에서 UART의 공식 모델을 구축 하시겠습니까?

Question

저는 교육에 대한 모델 검사와 NuSMV를 배우고 있습니다. 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 <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 구성 요소 모델링. 구문 론적 문제에 얽매이지 않도록 다른 형식주의로 구성 요소를 먼저 모델링하는 것이 도움이 될 수 있습니다. 구성 요소의 입력은 무엇입니까? 출력은 무엇입니까? 내부 상태가 있습니까? 내부 상태는 시간 경과에 따라, 특히 한 단계에서 어떻게 변하는가?

하드웨어 설명 언어 (예 : Verilog 및 VHDL)에 익숙한 경우 SMV의 전환이 시계 틱으로 볼 수 있기 때문에 이는 매우 좋은 출발점입니다. 당신이 그 언어를 모르는 경우에, 당신은 소프트웨어의 조각을 대신 쓰는 것을 시도 할 수있다; 이것은 시스템의 입출력을 이해하는 데 도움이되지만 SMV 로의 변환은 그렇게 직접적이지 않습니다.

매우 상태가 양호한 구성 요소의 경우 해당 자동 장치를 수동으로 그리면 도움이 될 수 있습니다.