SMV 소개 Konkuk Univ. IT 융합정보보호학과 오예원, 박선영
목차 SMV 소개 CTL NuSMV 설치방법및예시 (lift) 향후계획
SMV SMV(Symbolic Model Verifier) 는유한상태시스템 (finite state system) 이 CTL(Computation Tree Logic) 이라는논리와 BDD(Binary Decision Diagram) 를이용하여요구명세를만족하는지를자동적으로검증하는정형검증도구. CTL 을위한심볼릭모델체킹알고리즘을사용. SMV Input Language Finite State Kripke Structure Backend OBDD based Symbolic Model Checking Yes 모델을 BDD(Binary Decision Diagram) 로표현하고고정점계산으로속성의만족성여부를판정. Specification CTL Formula No CounterExample
CTL(Computation Tree Logic) CTL 의연산자들은주어진유한모델 (finite model) 의임의의한상태 (state) 가주어진논리식 (formula) 을만족하는지효율적으로알아볼수있는 fixed point 특성을가짐. 시간의흐름에따라발생가능한경로를트리로표현 A - 모든실행가능한경로에대해 E - 어떤실행가능한경로에대해
SMV System architecture Model checking System description and specification in SMV input language System model & Automata CTL formulas (Property) Model Checker with SMV Specification is True Specification is false SMV 는 CTL 이라는논리와 BDD 를이용하여주어진논리의참과거짓을판별하는방법이다.
SMV Variants Cadence SMV CMU SMV 옛날버전 GUI 없음 NuSMV 두개의버전 2.x: - 오픈소스 - 새로운기능 - BDD 와 SAT 기반 1.x: - 기존버전 - GUI 있음 GUI 있음 새로운언어사용
NuSMV 설치방법 Eclipse 에 nusmv 사용시 editing 을용이하게해주는플러그인사용. Eclipse 에 Xtext 와 nusmv 를추가설치. Step1. 프로그램설치 - nusmv 윈도우인스톨러설치 (2.5.4 windows, 64bit 버전이용 ) http://nusmv.fbk.eu/bin/bin_download2-v2.cgi - Eclipse Modeling Neon 32 비트설치 https://www.eclipse.org/downloads/download.php?file=/oomph/epp/neon/r2a/eclipse-instwin64.exe
NuSMV 설치방법 1 2 Eclipse Modeling Tools 다운로드 Eclipse 에서 Xtext 를설치하기위해모델링컴포넌트인스톨수행
NuSMV 설치방법 3 Xtext 설치 - edit 시하이라이트등의기능을함. 4 NuSMV Tools 0.1.0 & nuseen 설치 - NuSMV 관련설정을하기좋도록관련플러그인설치
NuSMV 설치방법 5 Xtext project 로프로젝트생성. 원하는폴더에.smv 로파일생성. 6 NuSMV 실행을위해 Run Configuration 에서 NuSMV Model 에설치한 nusmv 경로를지정.
NuSMV 설치방법 7 8 NuSMV 를 Run 한다. 커맨드창에명령어입력을통해결과를확인가능
NuSMV 예시 lift
NuSMV 예시 lift MODULE main VAR floor : 1..4; direction: {up, down }; request1 : boolean ; request2 : boolean ; request3 : boolean ; request4 : boolean ; ASSIGN init ( floor ) := 1; init (direction) := up; init ( request1 ) := FALSE ; init ( request2 ) := FALSE ; init ( request3 ) := FALSE ; init ( request4 ) := FALSE ; next ( direction ) := case direction=up & floor <4: floor + 1; -- 올라감 direction= down & floor >1: floor - 1; -- 내려감 TRUE : floor ; esac ; next (direction) := case direction=up & next ( floor )=4: down ; direction= down & next ( floor )=1: up; TRUE : direction; esac ; next ( request1 ) := case next ( floor )=1: FALSE ; -- 요청을삭제하거나 ( 이미 1 층 ) request1 : TRUE ; -- 요청을가지고있거나 TRUE : {FALSE, TRUE };-- 동작을수행할수있음 esac ; next ( request2 ) := case next ( floor )=2: FALSE ; request2 : TRUE ; TRUE : {FALSE,TRUE }; esac ; next ( request3 ) := case next ( floor )=3: FALSE ; request3 : TRUE ; TRUE : {FALSE, TRUE }; esac ; next ( request4 ) := case next ( floor )=4: FALSE ; request4 : TRUE ; TRUE : {FALSE, TRUE }; esac ; SPEC AG!( direction=up & floor =4) SPEC AG!( direction= down & floor =1) SPEC AG( request1 -> AF! request1 ); SPEC AG( request2 -> AF! request2 ); SPEC AG( request3 -> AF! request3 ); SPEC AG( request4 -> AF! request4 );
NuSMV 예시 lift *** This version of NuSMV is linked to the MiniSat SAT solver. *** See http://www.cs.chalmers.se/cs/research/formalmethods/minisat *** Copyright (c) 2003-2005, Niklas Een, Niklas Sorensson NuSMV > go NuSMV > pick_state -r NuSMV > print_current_state -v Current state is 1.1 floor = 1 direction = up request1 = FALSE request2 = FALSE request3 = FALSE request4 = FALSE NuSMV > simulate -r -k 4 ******** Simulation Starting From State 1.1 ******** NuSMV > show_traces -t There is 1 trace currently available. NuSMV > show_traces -v <!-- ################### Trace number: 1 ################### --> Trace Description: Simulation Trace Trace Type: Simulation -> State: 1.1 <- floor = 1 direction = up request1 = FALSE request2 = FALSE request3 = FALSE request4 = FALSE -> State: 1.2 <- floor = 2 direction = up request1 = FALSE request2 = FALSE request3 = TRUE request4 = FALSE -> State: 1.3 <- floor = 3 direction = up request1 = TRUE request2 = FALSE request3 = FALSE request4 = FALSE -> State: 1.4 <- floor = 4 direction = down request1 = TRUE request2 = TRUE request3 = FALSE request4 = FALSE -> State: 1.5 <- floor = 3 direction = down request1 = TRUE request2 = TRUE request3 = FALSE request4 = FALSE
향후계획 모델 : Smart Elevator 요구사항 Door 설치 층수증가 Deadlock 상태검증 Elevator 대수증가에따른우선순위구성
감사합니다