DBPIA-NURIMEDIA

Size: px

Start display at page:

Download "DBPIA-NURIMEDIA"

우림 제
5 years ago
Views:

1 642 정보과학회논문지 : 소프트웨어및응용제 30 권제 7 호 (2003.8) SMV 를이용한유한상태기계의동치검사 (Equivalence Checking of Finite State Machines with SMV) 권기현 엄태호 (Gihwon Kwon) (Tae-Ho Eom) 요약본연구에서는유한상태기계들간의동치여부를검증하고자한다. 즉모든입력에대하여유한상태기계의반응이항상동일한지를판정하고자한다. 만약두개의유한상태기계가동치라고판정된다면, 복잡한유한상태기계는단순한기계로대치될수있다. 또한명세와구현이모두유한상태기계로표현된경우, 동치검사를이용해서구현이명세를만족하는지결정할수있다. 본논문에서는이와같은유한상태기계의동치검사를모델검사기법으로다음과같이해결한다. 주어진유한상태기계 M A 와 M B 를조합하여모델 M = M A M B 을구축하고, 검사할동치조건을시제논리식 로기술한다. 만일모델이시제논리식을만족한다면 (M ) 두기계는동치이다. 그렇지않다면두기계는비동치이며그이유를설명하는반례를제공한다. 전과정이자동화되었으며, 여러개의사례연구에적용한결과만족할만한결과를얻었다. 키워드 : 유한상태기계, 동치검사, 곱기계, 모델검사, 시제논리 Abstract In this paper, we are interested in checking equivalence of FSMs(finite state machines). Two FSMs are equivalent if and only if their responses are always equal with each other with respect to the same external stimuli. Equivalence checking FSMs makes complicated FSM be substituted for simpler one, if they are equivalent. We can also determine the system satisfies the requirements, if they are all written in FSMs. In this paper, we regard equivalence checking problem as model checking one. For doing so, we construct the product model M = M A M B from two FSMs M A and M B. And we also get the temporal logic formula from the equivalence checking definition. Then, we can check with model checker whether M satisfies, written M. Two FSMs are equivalent, if M. Otherwise, it is not equivalent. In that case, model checker generates counterexamples which explain why FSMs are not equivalent. In summary, we solve the equivalnce checking problem with model checking techniques. As a result of applying to several examples, we have many satisfiable results. Key words :Finite state machine, Equivalence checking, Product machine, Model checking, Temporal logic 1. 서론 유한상태기계는시스템의행위를모델하는모델링언어이다 [1, pp ]. 다른모델에비해서단순하고이해하기쉬울뿐만아니라, 타겟언어의코드로쉽게변환될수있다. 이러한이점때문에반응형시스템및실시간시스템의행위를기술하는데널리사용되고 본연구는전자통신연구원위탁과제 ( ) 연구비지원으로수행되었음 종신회원 : 경기대학교정보과학부교수 khkwon@kuic.kyonggi.ac.kr 비회원 : 경기대학교전자계산학과 ever9@kyonggi.ac.kr 논문접수 : 2002년 11월 29일심사완료 : 2003년 03월 19일 있으며, 표현력을높이기위해유한상태기계를확장한다양한모델링언어들이 ( 예를들어 Statechart [2], RSML [3], SCR [4]) 산업현장에서활발히사용중이다. 유한상태기계에대한대표적인검사로동치검사가있다. 동치검사란, 모든입력에대해서주어진두유한상태기계의출력이항상동일한지를판정하는것이다 [5]. 예를들어, 그림 1에있는유한상태기계 M A 와 M B 에 이입력되면두기계의출력은 으로동일하다. 어떠한입력을주더라도두기계의출력이항상동일하기때문에 M A 와 M B 는동치이다. 이와같은동치검사는시스템최적화및정확성확인등에활용될수있다 [6]. 만약두개의유한상태기계가동치라고판정된다면, 복잡한유한상태기계는

2 SMV 를이용한유한상태기계의동치검사643 그림 1 예제 : 유한상태기계 M A, M B 보다단순한기계로대치될수있다. 또한명세와구현이모두유한상태기계로표현된경우, 동치검사를이용해서구현이명세를만족하는지를결정할수있다. 본논문에서는하드웨어및소프트웨어검증에널리사용되고있는모델검사기법을이용하여유한상태기계의동치검사를다음과같이수행한다. 먼저, 주어진유한상태기계 M A 와 M B 를조합하여 M = M A M B 을구축하고, 동치가되기위해반드시만족해야할조건을시제논리식 로표현한다. 그런후, 모델검사를이용하여모델 M이시제논리식 를만족하는지를검사한다 [7]. 만약 M 1) 이면두기계는동치이고 ( 그이유에대한상세한설명은 3장을참조하기바람 ), 그렇치않다면두기계는비동치이며모델검사에의해서생성된반례를통하여비동치의원인을파악할수있다. 본논문의구성은다음과같다. 2장에서는동치검사와관련된기본개념을다루며, 3장에서는동치검사문제를모델검사문제로변환하는과정을기술한다. 4장에서는유한상태기계를 SMV 언어로변환하는규칙과시스템구현을설명하며그리고본방법의효과를분석한다. 마지막으로 5장에서결론을맺는다. 2. 동치검사문제 유한상태기계 M A, M B 가동치라면 M A M B 라고표시하자. 본절에서는 M A M B 를판정하는동치검사의원리를설명하고필요한기본개념을기술한다. 정의 1: 유한상태기계는다음과같이 6-튜플 (I, O, S, d,, ) 로정의된다. - I 는입력집합이다. - O 는출력집합이다. - S 는상태집합이다. - d S는초기 (default) 상태이다. - : I S S는천이함수이다. 다음상태 s' S 는입력 i I 와현재상태 s S 에의해서결정된다. 즉 (i, s) = s' 이다. 1) 모델검사에서는 'M 이 를만족한다 ' 를 M 로표기한다. 여기서기호 는 ' 만족성관계 ' 를나타낸다. - : I S O 는출력함수이다. 출력 o O 는입력과현재상태에의해서결정된다. 즉 (i, s) = o 이다. 만일유한상태기계들의입력과출력공간이동일하다면, 두기계의동치여부를검사하는것이가능하다. 동치검사를위해서두기계를조합한곱기계를아래와같이구성한다. 정의 2: 두개의유한상태기계 M A = (I A, O A, S A, d A, A, A) 와 M B = (I B, O B, S B, d B, B, B) 가주어졌을때, 곱기계 M = M A M B = (I, O, S, d,, ) 는다음과같다. - I = I A = I B 입력집합이다. - O = {0,1} 은출력값이다. 단 O A = O B 이다. - S = S A S B = {(s A,s B) s A S A, s B S B} 는상태쌍들의집합으로서두기계에있는상태들의곱이다. s = (s A,s B) 는곱기계의임의의상태를나타낸다. - d S은곱기계의초기상태를나타낸다. 여기서 d = (d A,d B) 이다. - : I S S 는천이함수로서, 다음상태는입력과현재상태에의해서결정된다. 즉 (i,(s A,s B)) = ( A(i,s A), B(i,s B)) 이다. - : I S O 는출력함수로서, 상태 s 에서입력 i 에대해서두기계의출력값이같으면 1 을, 그렇지않으면 0을출력한다. 즉 (i,s) = A (i,s A) B(i,s B) 이다. 정의에서보듯이, 출력함수 는곱기계의상태 s에서하나의입력 i에대해서두기계의출력이동일한지를판정한다. 상태 s 에서모든입력에대해두기계의출력이동일한지를판정하는것은다음과같다. 정의 3: E(s) 는곱기계의상태 s = (s A,s B) 에서모든입력값 i에대해서두기계의출력이같음을 E(s) = i A(i,sA) B(i,s B) 나타내는술어이다. 두기계가동치이기위해서는, 곱기계의초기상태로부터도달가능한모든상태에서두기계의출력이동일해야한다. 즉도달가능한모든상태에서 E(s) 가만족되어야한다. 따라서동치관계의정의는다음과같다. 정의 4: 곱기계의초기상태 d로부터도달가능한모든상태집합을 P(d) 라고하자. 동치이기위해서는, 도달가능한모든상태에서두기계의출력이동일해야한다. 즉, d S s S s P(d) E(s)

3 644 정보과학회논문지 : 소프트웨어및응용제 30 권제 7 호 (2003.8) 이다. 그러므로곱기계의초기상태 d로부터도달가능한상태들을방문해가면서, 매상태마다 E(s) 가만족되는지를검사함으로서동치여부를판정할수있다. 동치검사를수행하기위해서현재상태에서도달가능한다음상태들의집합을계산해야한다. 이것을상계산 (image computation) 이라고한다 [7]. 상계산은현재상태에서한번의전이를통해서이동할수있는다음상태들의집합을구하는작업이다. 초기상태 d로부터고정점 (fixed point) 에도달할때까지반복적으로상계산을적용하면, 도달가능한상태집합 P(d) 를얻을수있다. 새로운상태를구할때마다 E(s) 를검사한다. E(s) 를만족하지않는상태가하나라도존재하면, 두기계는비동치이기때문에반례를출력하고즉시중지한다. E(s) 를만족한다면, 고정점에도달할때까지이과정을반복수행한다. 고정점에도달할때까지모든상태가 E(s) 를만족하면두기계는동치이다. 3. 모델검사를이용한동치검사문제해결본연구에서는동치검사문제를모델검사기법으로해결한다. 먼저전장에서살펴본유한상태기계의동치조건을시제논리식으로변환하는과정은다음과같다. 정의 4에의하면동치조건은 d S s S s P(d) E(s) 이다. 정의 3을이용해서 E(s) 부분을치환하면 d S s S s P(d) ( i A(i,s A) B(i,s B)) 을얻는다. 초기상태는항상존재하기때문에 -제거규칙 ( -elimination rule, [8]) 를이용하여 s S s P(d) ( i A(i,s A) B(i,s B)) 앞쪽에있는 한정사를제거한다. ' 모든가능한입력 ' 을나타내는뒤쪽의 는 -제거규칙 ( -elimination rule, [8]) 를이용하여 s S s P(d) ( A(i,s A) s(i,s B)) 제거한다. 맨앞의 s S s P(d) 은 'for every reachable state( 도달가능한모든상태 )' 를나타내기때문에, 위의식을 for every reachable state, A(i,s A) B(i,s B) 로개서할수있다. 시제논리언어인 CTL (Computation Tree Logic, [9]) 연산자중에서 AG는 'for every reachable state' 를나타낸다. 따라서위의식을 CTL 시제논리식으로나타내면 AG( A(i,s A) B(i,s B)) 이다. 정리 1: 두개의유한상태기계 M A, M B 와곱기계 M = M A M B 가주어졌을때, 다음은 M A M B iff M AG( A(i,s A) B(i,s B)) 성립한다. 증명 : 증명은매우직관적이다. 먼저좌변에서우변으로증명을한다. 두기계가동치라면, 두기계를조합한곱기계의모든도달가능한상태에서어떠한값이입력되더라도두기계의출력은같다. 따라서좌변에서우변으로는참이다. 우변에서좌변으로증명도이와비슷하다. 정리에의해서, 동치검사를모델검사로해결할수있게되었다. 모델검사를이용하여동치검사를수행하는방법및예제를살펴보면다음과같다. 먼저모델 M 에서 CTL 식 를만족하는상태집합을 라고하자. 만일초기상태가 에포함된다면 M 이고, 포함되지않는다면 M 이다. 그러므로모델검사알고리즘의핵심은 을구하는것이다 [7]. 이를위해서역방향탐색 (backward search) 함수 pre 를다음과같이 pre (Q) = {s S s' if (i,s,s') then s' Q} 정의한다. 함수 pre 는집합 Q로만천이되는이전상태들을리턴한다. 함수 pre 와최대고정점을이용하여동치조건 AG( A(i,s A) B(i,s B)) 을만족하는상태집합을아래와같이 AG( A(i,s A) B(i,s B)) = Z.( A(i,s A) B(i,s B) pre (Z)) 계산할수있다. 여기서 는최대고정점이다. 최대고정점계산을이용하여 = AG( A(i,s A) B(i,s B)) 를만족하는상태집합을계산한후, 초기상태포함유무를통해서 M A M B if d (M 인경우 ) M A M B otherwise (M 인경우 ) 두기계의동치여부를판정할수있다. 예제 1: 그림 1에주어진유한상태기계 M A 와 M B 로부터곱기계 M을구축하면그림 2와같다. 각기계의상태수가 3과 4이기때문에곱기계의상태수는 3*4=12 이다. M에서동치조건인 AG( A(i,s A) B(i,s B)) 를만족하는상태들의집합은다음과같다 : AG( A(i,s A) B(i,s B)) = Z.( A(i,s A) B(i,s B) pre (Z)) ={(s 0,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} 왜냐하면, 최대고정점 Z.( A(i,s A) B(i,sS) pre (Z)) 의계산이아래와같기때문이다.

4 SMV 를이용한유한상태기계의동치검사 SMV 를이용한동치검사 0 그림 2 곱기계 M = M A M B = S 1 = A(i,s A) B(i,s B) pre ( 0 ) ={(s 0,t 0), (s 0,t 1), (s 1,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} S ={(s 0,t 0), (s 0,t 1), (s 1,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} 2 = A(i,s A) B(i,s B) pre ( 1 ) ={(s 0,t 0), (s 0,t 1), (s 1,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} {(s 0,t 0), (s 1,t 1), (s 1,t 2), (s 1,t 3), (s 2,t 1), (s 2,t 2), (s 2,t 3)} ={(s 0,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} 3 = A(i,s A) B(i,s B) pre ( 2 ) ={(s 0,t 0), (s 0,t 1), (s 1,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} {(s 0,t 0), (s 1,t 1), (s 1,t 2), (s 1,t 3), (s 2,t1), (s 2,t 2), (s 2,t 3)} ={(s 0,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} = 2 (s 0,t 0) AG( A(i,s A) B(i,s B)) 이기때문에곱기계모델은동치검사조건을만족한다. 따라서두기계 M A 와 M B 는동치이다. 그림 3에서보듯이고정점계산으로구해진 {(s 0,t 0), (s 1,t 1), (s 2,t 2), (s 2,t 3)} 집합은초기상태로부터도달가능한상태집합이다. 그림 3 초기상태로부터도달가능한상태집합 전장에서동치검사를모델검사로해결할수있는이론적인배경을살펴보았다. 본장에서는모델검사도구인 SMV(Symbolic Model Verifier, [10]) 를이용하여동치검사를수행하는과정을기술한다. 유한상태기계를 SMV로변환하는규칙과시스템구현사항을차례대로기술한다. 4.1 SMV 입력언어로의변환규칙 SMV 에서는개별적으로정의된각기계의상태는내부적으로상태들의카테시안곱을형성한다. 예를들어두개의집합 S A = {s 1,,s n}, S B = {t 1,,t m} 으로각기계의상태를정의하면, SMV 내부에서는이들의곱상태 {(s 1,t 1),,(s n,t n)} 를갖는다. 이러한 SMV 특성을이용한다면유한상태기계로부터 SMV 코드를생성하는변환규칙을간단히기술할수있다. 아래의변환규칙은 M A 의변환규칙만을다룬다. 먼저변환규칙 1-3은변수선언을나타낸다. 규칙 4-6은초기값, 상태천이, 그리고출력함수를기술하는규칙이다. 규칙 7은검사할동치조건을 SMV로변환한다. 규칙 1: 유한상태기계는여러개의상태중하나의상태에만머무르기때문에상태집합 S A = {s 1,,s n} 는열거형 (enumeration type) 으로변환한다. VAR S A:{s 1,,s n}; 규칙 2: 입력집합 I = {i 1,,i m} 는두기계에서같으며, 하나의입력만이선택되므로열거형으로변환한다. VAR I : {i 1,,i m}; 규칙 3: 출력집합 O A = {o 1,,o k} 는입력집합과마찬가지로열거형으로변환한다. 그러나동치를위해각기계의출력값을비교해야하므로각기계마다따로출력값을선언한다. 그리고초기의출력값이미정의되어있기때문에이를고려해서아래와같이변환한다. VAR O A: {0,o 1,,o k}; 여기서, 0은미정의를나타낸다. 규칙 4: 입력은외부환경에서주는것이므로비결정적으로처리해야한다. SMV에서는아무런값을배정하지않음으로서비결정성을기술할수있다. 입력을비결정적으로다루기위해서초기값과다음상태값을고의적으로지정하지않는다. 그러나출력의경우, 초기값이미정의되어있기때문에 0을배정한다. 시작상태는 d A S로배정하면된다. 따라서초기값은다음과같이표현된다. INIT S A = d A & O A = 0 규칙 5: 정의에의하면상태천이함수는 (i, s) =

5 646 정보과학회논문지 : 소프트웨어및응용제 30 권제 7 호 (2003.8) s' 이다. 즉, 다음상태는현재상태와입력에의해서결정된다. M A 의상태천이를나타내는식은 i I, s S A (I = i S A =s next(s A )= (i, s)) 이며, SMV 표현은다음과같다. TRANS ((I=i 1 & S A = s 1 & next(s A)=s') (I=i 1 & S A = s n & next(s A)=s') (I=i 2 & S A = s 1 & next(s A)=s') (I=i m & S A = s n & next(s A)=s')) 규칙 6: 정의에의하면출력함수는 (i, s) = o이다. 즉, 현재상태와입력에의해서출력값이결정된다. M A 의출력을나타내는식은 i I,s S A (I = i S A =s next(o A )= (i, s)) 이며, SMV 표현은다음과같다. TRANS ((I=i 1 & S A = s 1 & next(o A)=o) (I=i 1 & S A = s n & next(o A)=o) (I=i 2 & S A = s 1 & next(o A)=o) (I=i m & S A = s n & next(o A)=o)) 규칙 7: 전장에서살펴본바와같이두기계의동치조건은 AG( A(i,s A) B(i,s B)) 이다. 즉두기계의출력이도달가능한모든상태에서동일해야한다는것이다. 이것을 SMV 입력언어로변환하면다음과같다. DEFINE equivalence := O A <-> O B; SPEC AG equivalence 4.2 구현및분석변환규칙을이용하여유한상태기계로부터 SMV 코드를자동변환하였다. 전체시스템의개요및입력텍스트파일은그림 4, 그림 5와같다. 유한상태기계를기술한텍스트파일을받아서유한상태기계, 크립키구조 (Kripke structure, [7]), 그리고곱크립키구조를차례대로구축한다. 그런다음에변환그림 4 변환시스템 그림 5 유한상태기계 M A 와 M B 를기술한텍스트파일 규칙을적용하여 SMV 코드를최종적으로생성한다. 그림 5에있는 M A 와 M B 의텍스트파일로부터 SMV를코드를생성하여실행시킨결과가그림 6에있다. 그림에서보듯이, 곱크립키구조의전체상태수는 96개이며, 2) 검사에소요된시간은 0.01초이었다. 이와같은방법으로여러개의유한상태기계에대해서동치검사를수행하였고그결과는표 1과같다. 다루었던예제중에서모델 7이가장복잡했다. 모델 7 의경우변환된 SMV 코드의행수는 6,958행이었고생성된전체상태수와도달가능한상태수가각각 2 54 및 2 11 였지만, 수행시간은 1초이내로 (0.84초) 만족스러웠다 ( 모델 7의경우 M A 와 M B 는동일한모델이다. 동일한모델을검사하면그결과는당연히동치이기때문에, 동일한모델은동치검사의가장간단한시험사례라고할수있다 ). 그림 6 SMV 를이용하여두기계의동치검사결과 2) 유한상태기계가고급언어라면, 크립키구조는저급언어이다. 고급언어의한문장이변환될때저급언어의여러문장이필요하다. 유한상태기계와크립키구조도이와비슷하다. 2장에서살펴본대로 M A 와 M B 의곱기계의상태수는 3*4=12 이다. 그러나 M A 와 M B 의곱크립키구조의상태수는 2*2*2*3*4=96 이다. 2, 2, 2, 3, 4는각각입력수, M A 의출력수, M B 의출력수, M A 의상태수, M B 의상태수이다.

6 SMV 를이용한유한상태기계의동치검사647 유한상태기계 상태수 천이수 표 1 실행결과분석 입력수 출력수 SMV 라인수 모델1 MA M B 모델2 MA M B 모델3 MA M B 모델4 MA M B 모델5 MA M B 모델6 MA M B 모델7 MA M B 전체상태공간 48 ( 2 6 ) 32 ( 2 5 ) 96 ( 2 7 ) 96 ( 2 7 ) 1440 ( 2 10 ) 1296 ( 2 10 ) e+16 ( 2 54 ) 수행도달한시간상태수 ( 단위초 ) 8 ( s ) 8 ( 2 3 ) 10 ( 2 3 ) 8 ( 2 3 ) 48 ( 2 6 ) 48 ( 2 6 ) 2049 ( 2 11 ) 0.04s 0.01s 0.01s 0.06s 0.09s 0.84s 한편, 유한상태기계가비동치인경우 SMV는반례를생성한다. 반례를통해서비동치의원인을파악할수있다. 예를들어, 그림 7에있는두기계 M A 와 M B 를살펴보자 ( 표 1의모델 6에해당 ). SMV 코드를자동생성하여실행한결과 AG equivalence 는거짓이었으며, 비동치의원인을설명하는반례가그림 8과같이생성되었다. 반례중에서두기계의상태가각각 s6, t6인경우를보자 ( 그림 8에서 state1.8 에해당 ). 가능한입력수가총 4개 (00, 01, 10, 그리고 11) 이기때문에두개의부울변수 in0, in1으로입력을나타낸다. state1.8 에서 in0가 0으로변경되었고 in1은계속해서 1을유지하기때문에현재입력은 01이된다. 따라서상태천이가발생해서두기계의상태는각각 s7, t7이된다 (state1.9 에해당 ). 입력변수에대해서아무런변경이없기때문에, 현재입력은다시 01이된다. 따라서두기계의상태는 s7, t7에서 s6, t6로각각천이되지만, 이때출력은 1과 0으로서로다르다. 따라서비동치임을알리고종료한다. 그림 7 비동치관계에있는유한상태기계 M A 와 M B -- specification AG equivalence is false -- as demonstrated by the following execution sequence state 1.1: equivalence = 1 MA = s0 MB = t0 in1 = 0 in0 = 0 OA0 = 0 OB0 = 0 state 1.2: in0 = 1 state 1.3: MA = s1 MB = t1 in1 = 1 state 1.4: MA = s2 MB = t2 in0 = 0 state 1.5: MA = s3 MB = t3 in1 = 0 state 1.6: MA = s4 MB = t4 in0 = 1 OA0 = 1 OB0 = 1 state 1.7: MA = s5 MB = t5 in1 = 1 state 1.8: MA = s6 MB = t6 in0 = 0 state 1.9: MA = s7 MB = t7 state 1.10: equivalence = 0 in1 = 0 OB0 = 0 그림 8 비동치의원인을설명하는반례

7 648 정보과학회논문지 : 소프트웨어및응용제 30 권제 7 호 (2003.8) 5. 결론 요약하자면, 본연구에서는유한상태기계의동치검사 (M A M B) 를모델검사 (M ) 로해결했다. 검사될두기계를카테시안곱해서모델 M을얻었고, 두기계의동치조건을정의한후이를 CTL 식 로표현하였다. 그런후, 모델검사를 (M ) 통해서두기계의동치여부를판정하였다. 유한상태로부터 SMV 코드를생성하는변환규칙을제시하고, 변환시스템을구현하였다. 여러개의예제에본시스템을적용해본결과동치와비동치를정확하게구분하였다. 다루었던예제중에서가장큰상태수가 2 54 였지만수행시간은 1초이내로만족스러웠다. 이와같은유한상태기계의동치검사는시스템최적화및정확성확인등에활용될수있다. 만약동치라고판정된다면, 복잡한유한상태기계는단순한기계로대치될수있다. 또한명세와구현이모두유한상태기계로표현된경우, 동치검사를이용해서구현이명세를만족하는지를결정할수있다. 전술한바와같이, 본연구에서는 Clarke [7] 등이제시한시제논리모델검사기법을동치검사 [11,12] 문제에응용하였다. 그결과동치검사시스템을새롭게개발하기보다는, 범용모델검사도구인 SMV 를사용하여동치검사를자동화할수있었다. 동치검사와관련해서앞으로계속연구해야할내용은다음과같다. 첫째, SMV 대신최근에활발히연구되고있는 BMC (Bounded Model Checker, [13]) 등을이용하여동치검사를수행하는것이다. 둘째, 유한상태기계보다표현력이높은상태도를동치검사하는것이다. 참고문헌 [1] R. Skvarcius and W.B. Robinson, Discrete Mathematics with Computer Science Applications, The Benjamin/Cummings Publishing Company, [2] D. Harel and A. Naamad, "The STATEMATE Semantics of Statecharts," ACM Transactions on Software Engineering and Methodology, Vol.5, No. 4, pp , [3] David Y.W. Park, et.al., "Static Analysis to Identify Invariants in RSML Specifications," In Proceedings of Formal Techniques in Real-Time and Fault-Tolerant'98, LNCS 1486, [4] C. Heitmeyer, et.al., "Using Abstraction and Model Checking to Detect Safety Violations in Requirements Specifications," IEEE Transactions on Software Engineering, Vol.24, No.11, [5] S.Y. Huang, K.T. Cheng, K.C. Chen, C.Y. Huang, and F. Brewer, "AQUILA: An Equivalence Checking System for Large Sequential Designs," IEEE Transactions on Computer, Vol.49, No.5, pp , [ 6 ] Robert Meolic, Tatjana Kapus, Zmago Brezocnik, "Computing Testing Equivalence with Binary Decision Diagrams," In Proceedings of the Seventh Electrotechnical and Computer Science Conference ERK'98, pp.51-54, [7] E.M. Clarke, O. Grumberg, and D. Peled, Model Checking, MIT Press, [8] M. Huth and M. Ryan, Logic in Computer Science : Modelling and Reasoning about Systems, Cambridge University Press, [9] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications," ACM Transactions on Programming Languages and Systems, Vol.8, No.2, pp , [10] K.L. McMillan, "Symbolic Model Checking: An approach to the state explosion problem," PhD thesis, Carnegie Mellon University, [11] C.A.J. van Eijk and J.A.G. Jess, "Detection of Equivalent State Variables in Finite State Machine Verification," In Proceedings of the 1995 ACM/IEEE International Workshop on Logic Synthesis, pp , [12] C.A.J. van Eijk and J.A.G. Jess, "Exploiting Functional Dependencies in Finite State Machine Verification," In Proceedings of the European Design and Test Conference ED&TC, pp.9-14, [13] A. Biere, A. Cimatti, E.M. Clarke, and Y. Zhu, "Symbolic Model Checking without BDDs," In Proceedings of Tools and Algorithms for the Analysis and Construction of Systems (TACAS '99), LNCS 1579, 권기현 정보과학회논문지 : 소프트웨어및응용제 30 권제 3 호참조 엄태호 2001 년 2 월경기대학교정보과학부이학사 년 2 월경기대학교전자계산학과이학석사 년 3 월경기대학교전자계산학과박사과정

PowerPoint 프레젠테이션

PowerPoint 프레젠테이션 SMV 소개 Konkuk Univ. IT 융합정보보호학과 오예원, 박선영 목차 SMV 소개 CTL NuSMV 설치방법및예시 (lift) 향후계획 SMV SMV(Symbolic Model Verifier) 는유한상태시스템 (finite state system) 이 CTL(Computation Tree Logic) 이라는논리와 BDD(Binary Decision