SMV Vending Machine Implementation and Verification 201321124 김성민 201472412 정혁준 201472262 손영석 2015.05.04
Contents Review 지적사항 개선사항
Review
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
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
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 점등
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 점등
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 캔음료선택및판매
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 차음료선택및판매
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 투입금액환불
지적사항
지적사항 Module 일원화 SMV coding 기존코딩 Main 모듈에서각각의모듈을사용하나 Input_process 에서대부분의작업이일원화되어있다.
지적사항 Model Checking 기존 Model Checking 현재 step 에대해서만 checking 수행 Next step 에대한 checking 이없음
개선사항
개선사항 (module 세분화 ) main Run Vending Machine Control Select Can Maintain Stock refund Select Tea Check_can Check_tea Insert Coin
개선사항 - Code SMV coding 개선된코딩 Input_process 에일원화되어있던작업을기능별모듈로세분화하였다. runvendingmachine : 밴딩머신의세분화된작업이총괄적으로실행되는모듈
개선사항 - Code SMV coding
개선사항 Model Checking
개선사항 Model Checking 1. 자판기의반환버튼을누른후잔액은 0원이된다. 2. 자판기에서캔을선택한후캔이나온다 3. 동전을넣은후금액이반영된다 4. 캔을선택한후캔금액만큼차감된다.
개선사항 Model Checking 1. 자판기의반환버튼을누른후잔액은 0 원이된다. test11 : SPEC AG((state = ) & (input_button = refund) -> AX (coin = 0)) State 가 이면서 refund 버튼이눌렸을때다음 state 에서잔액은 0 원이다 TRUE!
개선사항 Model Checking 1. 자판기에서캔을선택한후캔이나온다 test12 : SPEC AG((input_button = select_can_0) & (led_can[0]) -> AX (led_out)) 선택가능 led 가 TRUE 이면서해당캔버튼을클릭했을시다음 state 에서캔이나온다. TRUE!
개선사항 Model Checking 1. 동전을넣었을시금액이반영된다 test13 : SPEC AG((coin < 500) & (input_button = coin_1) -> AX (coin = coin + 1);) 현재들어있는금액에최고한도보다작으면서 10 원을투입시다음 state 에서 10 원이추가가반영된다. TRUE!
개선사항 Model Checking 1. 캔을선택했을시캔금액만큼차감된다. test18 : SPEC AG((input_button = select_can_0) & (led_can[0]) -> AX (coin = coin pr ice_can[0])) 선택가능한캔을선택시다음 state 에서캔금액만큼차감된금액이반영된다. TRUE!