🔮 NuSMV – model-based 테스트 케이스 설계 자동화 도구

이 툴은 소프트웨어 테스팅 이론 수업에서 처음 접하게 되었고, model-based testing을 자동화해주는 도구이다. 과제를 위해 간단하게 배웠는데 테스트 케이스를 활용해야 하는 경우 실용적일 것 같아 정리해둔다.

🤔 NuSMV?

NuSMV는 Binary Decision Diagram(BDD)를 기반으로 한 최초의 모델 검사 도구인 SMV를 다시 구현, 확장한 것이다. 모델 확인을 위한 개방형 아키텍처를 가지고 있으며 CTL과 LTL 표현식을 지원한다. 간단히 말해 Model-based testing tool이라고 할 수 있다.

LTL?

LTL은 Linear time Temporal Logic의 약자로, 시제 논리를 의미한다. True/False에 시간을 도입한 개념이라고 생각하면 쉽다.

CTL?

CTL은 Computational Tree Logic의 약자로, 시제 논리의 한 종류이다. CTL에서는 시간의 흐름을 트리 구조로 표현한다. LTL에서 A와 E가 추가된 구문을 가진다.

Temporal logic statements

LTL

G (p->q) // G : 시간의 흐름과 무관하게 항상 참이다
F (p&&q) // F : 언젠가는 그렇다
p U q 	 // U : p가 true이다 until q가 true가 될 때까지
X p 	 // X : next step에서는 그렇다

CTL

AG (p->q) // A : 모든 possible execution
AF (p&&q)
A (p U q)
AX p
---
EG (p->q) // E : exist, 존재한다
EF (p&&q)
E (p U q)
EX p

Examples : CTL

EF p의 경우 (1), (2), (3) 모두 true이다. 언젠가 p가 되는 경로가 존재하기 때문이다.
반면 AF p는 (1)에서 false, (2), (3)에서는 true이다. (1)에서는 실행 경로 중 P를 거치지 않는 경로가 있기 때문이다. (2)와 (3)에서는 initial state가 P이기 때문에 어떤 실행 경로이든 무조건 P를 거친다.

Fixed-point computation for EF

위의 그림에서 EF p = { A, B, C }이다. 그 과정을 계산해보면 아래와 같다.

Calculate process : compute τ^n[y] such that
τ^n[y] = τ^(n+1)[y], where τ[y] = p ∨ EX y

1. τ[false] = p ∨ EX false = p -> { B } : 한 번에 도달 가능한 P가 true가 되는 지점
2. τ^2[false] = p ∨ EX p -> { B, A } : 두 번만에 도달 가능한 P가 true가 되는 지점
3. τ^3[false] = p ∨ EX (p V EX p) -> { B, A, C } : 세 번만에 도달 가능한 P가 true가 되는 지점

Fixed-point computation for EG

위의 그림에서 EG p = { A }이다. 그 과정을 계산해보면 아래와 같다.

Calculate process : compute τ^n[y] such that
τ^n[y] = τ^(n+1)[y], where τ[y] = p ∧ EX y

1. τ[true] = p ∧ EX true = p -> { A, B, C } : 0번 next까지 P = true인 지점
2. τ^2[true] = p ∧ EX p -> { A, B } : 1번 next까지 P = true인 지점
3. τ^3[true] = p ∧ EX (p ∧ EX p) -> { A } : 2번 next까지 P = true인 지점

🖲️ Install - Mac

1. NuSMV download link(https://nusmv.fbk.eu/downloads.html)에 접속한다.

2. Version 2.6.0 Without ZCHAFF 테이블에서 NuSMV-2.6.0-macosx64.tar.gz를 다운로드한다.
   

3. 원하는 폴더로 옮긴 후 압축을 해제해 NuSMV-2.6.0-Darwin 폴더가 생성되는 것을 확인한다.

4. 해당 폴더에 접근해 NuSMV/bin/NuSMV 파일이 있는 것을 확인한다.

5. 터미널을 열고 NuSMV를 실행한다. NuSMV가 있는 폴더에서 NuSMV 명령어로 실행하면 된다.

• 이때 NuSMV를 열 수 없다는 경고가 나타날 경우 시스템 설정에서 NuSMV를 허용해준다.
• Security & Privacy(보안 및 개인 정보 보호) > General(일반) > Allow Anyway를 선택해 허용한다.

6. 터미널에서 NuSMV 파일을 /usr/local/bin 디렉토리로 이동해 실행한다. sudo mv {NuSMV path}/NuSMV-2.6.0-Darwin/bin/NuSMV /usr/local/bin 명령어를 실행하면 이동할 수 있다.

7. /usr/local/bin 디렉토리로 이동해 NuSMV를 실행한다. 정상적으로 동작하면 잘 설치된 것이다.

🚀 How to use

Test generation through model checking

NuSMV는 model checking 결과가 false일 경우 counter example을 추출해준다. 이를 활용해 일부러 원하는 결과(테스트 케이스)를 counter example로 가지는 구문을 입력해 test case를 생성할 수 있다.

• State coverage : G (!state = S)
• Transition coverage : G (state = N1 -> !X state = T1)
• others(condition coverage, MC/DC coverage, etc.)

Model example - vending machine

아래는 초콜릿을 판매하는 자판기를 model로 작성한 vendingmachine.smv 파일이다.

MODULE main
  VAR
   state: {Initial, Ready, Inserting, Enabled, Emitting, Returning, Final};
   amount: 0..1500;
   coin : {100, 500}; 
   event: {NONE, On, Off, Insert, Choose, Complete};
   time : 0..11;
  DEFINE
   COST:= 500;

  ASSIGN
    init(amount):= 0;
    init(time):=0;
    init(state):= Initial;
    init(event):= NONE;

    next(state):= case
        state = Initial & event = On   : Ready;
        state = Ready & event = Insert : Inserting;
        state = Ready & event = Off    : Final;
        state = Inserting & amount < 500 & time < 10 : Inserting;
        state = Inserting & amount >= 500 : Enabled;
        state = Inserting & amount < 500 & time >= 10 : Returning;
        state = Enabled & event = Choose & time < 10  : Emitting;
        state = Enabled & time >=10    : Returning;
        state = Emitting & event = Complete & amount >0 : Returning;
        state = Emitting &  amount = 0 : Ready;
        state = Returning &  amount =0  : Ready;
        TRUE                                  : state;
    esac;

    next(amount):= case
        amount + coin > 1500 : amount;
        state = Initial & event = On   : 0;
        state = Enabled & event = Choose & time < 10 & amount -COST >=0  : amount - COST;
        state = Ready & event = Insert : amount+coin ;
        state = Inserting & event =Insert &  time < 10 : amount+coin;
        state = Returning & event = Complete  : 0;
        TRUE                                  : amount;
    esac; 
    
    next(time):= case
        time +1 > 10   : time;
        state = Initial & event = On   : 0;
        state = Ready & event = Insert : 0;
        state = Inserting & event = Insert & time < 10 : 0;
        state = Inserting & time < 10 : time +1;
        state = Inserting & amount >= 500 : 0;
        state = Enabled & event = Choose & time < 10  : 0;
        state = Enabled &  time < 10  : time+1;
        state = Returning & event = Complete  : 0;
        TRUE                                  : time;
    esac; 


LTLSPEC G(state != Inserting)
LTLSPEC G(amount < 500)
LTLSPEC G(state != Enabled)
LTLSPEC G(state != Emitting)
LTLSPEC G(state != Returning)

LTLSPEC G(state = Inserting ->  X (state = Enabled))

LTLSPEC G(amount > 500 -> F (state = Enabled))
LTLSPEC G(state = Enabled -> F (state = Ready))
LTLSPEC G(state = Ready -> amount = 0)

Execute

$ NuSMV -int // interactive mode - 명령어 창 열기
NuSMV> read_model -i {filename} // load model
NuSMV> go // execute
NuSMV> show_property // LTLSPEC 등의 property list
NuSMV> check_ltlspec -n {spec number} // 선택한 spec의 실행 결과를 보여줌

NuSMV> quit
NuSMV> reset

이를 실행하면 다음과 같이 표시되는 것을 확인할 수 있다.

model checking tool을 활용하면 model-based testing을 자동으로 만들어낼 수 있다. 복잡한 모델의 경우 힘들겠지만, 확실한 검증이 필요한 경우에는 실무에서 적용할 수 있을 것으로 보인다.

---

Reference : LTL and CTL