SMV Vending Machine Implementation and Verification 김성민 정혁준 손영석

Size: px

Start display at page:

Download "SMV Vending Machine Implementation and Verification 김성민 정혁준 손영석"

동주 방
4 years ago
Views:

1 SMV Vending Machine Implementation and Verification 김성민 정혁준 손영석

2 Contents Review 지적사항 개선사항

3 Review

4 Review sell_denied start coin {1, 5, 10, 50, 100} coin Ready Input_ select {can_0, can_1, can_2, can_3, tea_0, tea_1, tea_2, tea3} select_ product sell select_ product led_out stock_check refund refund coin_out Overview

5 Review start coin_1 (10 원동전투입 ) coin_1 coin = coin + 1 Ready Input_ coin_5 (50 원동전투입 ) coin_10 (100 원동전투입 ) coin_50 (500 원동전투입 ) coin_5 coin_10 coin = coin + 5 coin = coin + 10 coin_100 (1000 원권투입 ) coin_50 coin = coin + 50 동전투입 coin_100 coin = coin + 100

6 Review led_can_0 Ready Input_ if coin > can_price[0] & stock_can[0] > 0 if coin > can_price[1] & stock_can[1] > 0 if coin > can_price[2] & stock_can[2] > 0 led_can_1 led_can_2 if coin > can_price[3] & stock_can[3] > 0 led_can_3 캔음료재고검사및판매가능캔음료의 LED 점등

7 Review Ready Input_ if coin > tea_price[0] & stock_tea_coffee > amount_tea_coffee[0] & stock_tea_sugar > amount_tea_suagr[0] & stock_tea_cream > amount_tea_cream[0] & stock_tea_cocoa > amount_tea_cocoa[0] & stock_tea_yulmu > amount_tea_yulmu[0] & stock_water > 0 stock_cup > 0 if coin > tea_price[1] & led_tea_0 led_tea_1 if coin > tea_price[2] & led_tea_2 if coin > tea_price[3] & led_tea_3 차음료재료검사및판매가능차음료의 LED 점등

8 Review start select_can_0 (1 번캔음료선택 ) select_can_0 if led_can[0] Ready Input_ select_can_1 (2 번캔음료선택 ) select_can_2 (3 번캔음료선택 ) select_can_1 if led_can[1] if led_can[2] led_out select_can_2 (4 번캔음료선택 ) select_can_2 if led_can[3] coin = coin can_price[n] stock_can[n] = stock_can[n] - 1 select_can_3 캔음료선택및판매

9 Review start select_tea_0 (1 번차음료선택 ) select_tea_0 if led_tea[0] Ready Input_ select_tea_1 (2 번차음료선택 ) select_tea_2 (3 번차음료선택 ) select_tea_1 if led_tea[1] if led_tea[2] led_out select_tea_2 (4 번차음료선택 ) select_tea_2 if led_tea[3] coin = coin tea_price[n] stock_tea_coffee = stock_tea_coffee amount_tea_coffee[n] select_tea_3 stock_water = stock_water 1 stock_cup = stock_cup - 1 차음료선택및판매

10 Review start Ready Input_ refund refund coin_out_100 = coin / 100 coin_out_50 = (coin mod 100) / 50 coin_out_10 = ((coin mod 100) mod 50) / 10 coin_out_5 = (((coin mod 100) mod 50) mod 10) / 5 coin_out_1 = (((coin mod 100) mod 50) mod 10) mod 5 투입금액환불

11 지적사항

12 지적사항 Module 일원화 SMV coding 기존코딩 Main 모듈에서각각의모듈을사용하나 Input_process 에서대부분의작업이일원화되어있다.

13 지적사항 Model Checking 기존 Model Checking 현재 step 에대해서만 checking 수행 Next step 에대한 checking 이없음

14 개선사항

15 개선사항 (module 세분화 ) main Run Vending Machine Control Select Can Maintain Stock refund Select Tea Check_can Check_tea Insert Coin

16 개선사항 - Code SMV coding 개선된코딩 Input_process 에일원화되어있던작업을기능별모듈로세분화하였다. runvendingmachine : 밴딩머신의세분화된작업이총괄적으로실행되는모듈

17 개선사항 - Code SMV coding

18 개선사항 Model Checking

19 개선사항 Model Checking 1. 자판기의반환버튼을누른후잔액은 0원이된다. 2. 자판기에서캔을선택한후캔이나온다 3. 동전을넣은후금액이반영된다 4. 캔을선택한후캔금액만큼차감된다.

20 개선사항 Model Checking 1. 자판기의반환버튼을누른후잔액은 0 원이된다. test11 : SPEC AG((state = ) & (input_button = refund) -> AX (coin = 0)) State 가 이면서 refund 버튼이눌렸을때다음 state 에서잔액은 0 원이다 TRUE!

21 개선사항 Model Checking 1. 자판기에서캔을선택한후캔이나온다 test12 : SPEC AG((input_button = select_can_0) & (led_can[0]) -> AX (led_out)) 선택가능 led 가 TRUE 이면서해당캔버튼을클릭했을시다음 state 에서캔이나온다. TRUE!

22 개선사항 Model Checking 1. 동전을넣었을시금액이반영된다 test13 : SPEC AG((coin < 500) & (input_button = coin_1) -> AX (coin = coin + 1);) 현재들어있는금액에최고한도보다작으면서 10 원을투입시다음 state 에서 10 원이추가가반영된다. TRUE!

23 개선사항 Model Checking 1. 캔을선택했을시캔금액만큼차감된다. test18 : SPEC AG((input_button = select_can_0) & (led_can[0]) -> AX (coin = coin pr ice_can[0])) 선택가능한캔을선택시다음 state 에서캔금액만큼차감된금액이반영된다. TRUE!

PowerPoint 프레젠테이션

PowerPoint 프레젠테이션 Cadence SMV Vending Machine 김그린김바울 INDEX 1. Problem Analysis 2. Modeling 3. Model Checking 1. Problem Analysis Default Money Inserted Count Money Reject Money Cancel Give Change Default Not Enough Money