fFSM 모델의 정형 분석

(Formal Analysis of fFSM Model)

박사천․권기현

경기대학교 전자계산학과 소프트웨어공학전공

{sachem, khkwon}@kyonggi.ac.kr

요  약

하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)가 개발되었다. PeaCE에서 fFSM(flexible Finite State Machine)은 제어흐름을 명세하도록 풍부한 구문을 제공하는 모델이지만, 정형 의미의 부재로 인해서 명세를 정형 분석하기가 어려웠다. 본 논문에서는 fFSM에 대한 정형 의미를 정의했고, 이를 통해서 정형 분석을 수행하는 프레임워크를 개발했다. 본 논문에서 개발된 프레임워크를 통해서 데드락, 레이스 조건(race condition), 애매한 전이(ambiguous transition), 순환 전이(circular transition)등과 같이 임베디드 소프트웨어에서 발생할 수 있는 중요한 버그들을 정형적으로 분석하는 방법을 보인다.

1. 서  론

fFSM 모델의 정형 분석

프로그래밍언어논문지 제 권 제 호 (    . )

본 과제는 정보통신부 선도기반기술개발사업의 지원으로 수행되었습니다.

임베디드 시스템의 생산성 향상을 꾀하기 위해서, 하드웨어/소프트웨어 통합 설계가 새로운 설계 방법론으로 부각되고 있다. PeaCE[1]는 임베디드 시스템 개발을 돕기 위한 통합 설계 환경으로서, 알고리즘을 표현하기 위해 동기적 데이터 흐름(Synchronous Data Flow) 모델을 사용하고 제어 흐름을 모델링하기 위해 확장된 유한 상태 기계인 fFSM 모델을 사용한다. 또한 두 모델들에 대한 시스템 수준의 조화를 위해서 작업-수준(task-level) 명세를 사용한다.

fFSM은 확장된 유한 상태 기계의 일종으로서 하렐의 상태도(Statechart)와 같이 동시성, 계층성, 내부 이벤트, 그리고 전역변수를 포함한다 [2]. 이 모델은 STATEMATE[3]와 Ptolemy[4]의 영향을 받았다. 그러나 아직 내부 모델들(SDF, fFSM)에 대한 정형 의미가 명시적으로 정의되지 않았다. 특별히 fFSM의 경우 정형의미의 부재로 인해 시스템을 정형적으로 분석할 수 없었다.

따라서 이 논문에서는 신뢰성 있는 코드 생성과 모델의 정형 검증의토대가 되는 fFSM 모델을 위한 단계 의미를 정의하고 그에 대한 검증 방법을 소개한다. 특히 임베디드 시스템의 정형 검증이 매우 어려운 만큼 본 논문에서는 사용자가 쉽게 접근할 수 있는 방법을 제안한다.  본 논문에서 제안하는 단계 의미는 이벤트가 발생될 때, 한 형상(Configuration)에서 다른 형상으로 변해가는 과정을 정의하고, 동시에 출력 이벤트와 내부 이벤트, 전역변수의 갱신으로 구성된 액션을 정의한다. 이 분야에 이미 많은 제안들이 있었지만, fFSM의 정형 의미를 정의하기 위해서 확장된 계층적 오토마타(Extended Hierarchical Automata, 이하 EHA라 부름, [5])와 계층적 상태/이벤트 모델(Hierarchical State/Event Model, 이하 HSEM라 부름, [6])]의 의미를 참조 하였다.

EHA는 1996에 제안되어 STATEMATE에서 이용되는 상태도의 의미를 정형적으로 정의하는데 사용되었다. EHA의 의미는 전진 규칙(progress rule), 멈춤 규칙(stuttering rule), 결합 규칙(composition rule)의 세 가지 규칙으로 정의된다. 만일 활성화된 전이가 실행된다면, 그 오토마타에서 전진 규칙이 선택된다. 그런데 오토마타에서 활성화된 상태가 기본 상태이고 활성화된 전이가 없다면 이벤트를 소모시키는 멈춤 규칙이 적용되고, 최상위로부터 각각의 하위 오토마타에 모두 이 규칙들이 적용된 후 결합규칙에 의해서 그 결과가 도출된다.

HSEM은 UML(Unified Modeling Language)에 기반한 상태도의 변종으로 IAR visualSTATE[7]에서 사용되고 있다. 이 모델에서는 행위를 N개의 평탄화한 병렬 기계로 나타내는데 여기서 N은 상태도로 보면 OR-상태의 수에 해당한다. 따라서 HSEM의 형상은 정확히 N개로 구성되고 그렇기에 형상에 비 활성화된 상태들도 포함하게 된다. 이렇게 표현된 모델은 기호적 모델검사와 상태폭발 방지 기법 중 하나인 결합 모델체킹(compositional model checking)에 용이하다.

이 논문에서는 PeaCE에서 사용되는 fFSM의 의미를 정의하기 위해 EHA과 HSEM의 의미를 참조하였다. 정의된 의미를 바탕으로 fFSM 모델은 모델 체커인 SMV의 입력 언어로 자동으로 변환되고, 임베디드 시스템 검증에 주로 이용되는 6가지 속성들을 푸쉬버튼 방식으로 SMV의CTL(Computation Tree Logic) 속성으로 자동 변환하여 사용자가 쉽게 검증을 수행할 수 있는 도구를 개발했다.

본 논문의 구성은 다음과 같다. 2 장에서는 fFSM 모델을 설명하고 fFSM의 평탄화된 병행기계인 pFSM의 구문을 정의한다. 3장에서는 pFSM의 단계의미를 정의하고 4장에서는 임베디드 시스템에서 검증해야 하는 주요 속성에 대해 설명하고, 그 속성이CTL 논리로 자동 변환되는 과정과 pFSM이 SMV로 변환되는 과정을 설명한 후 시뮬레이션과 모델체킹을 통한 버그 검출 결과를 소개한다. 마지막으로 5장에서 결론 맺고 향후 연구 주제에 대해 언급한다.

2. 제어흐름 모델의 구문

2.1. fFSM 구문

정의 1 (flexible FSM) fFSM은 [eqn: fF] = [eqn: (][eqn: I], [eqn: O], [eqn: I T] [eqn: IT], [eqn: X], [eqn: V], [eqn: F][eqn: )]로 정의된다. [eqn: I], [eqn: O], [eqn: I T]는 이벤트들의 집합, [eqn: X]는 상태들의 집합, [eqn: V]는 변수들의 집합 그리고 [eqn: F]는 전이들의 집합이다. 이벤트 [eqn: e]는 [eqn: (e _{n} ,```e _{v} )]로 정의되는데, en은 이벤트의 이름이며, [eqn: e _{v}]에서 허용하는 값의 범위이다. [eqn: I] = [eqn: left{][eqn: (][eqn: i _{n _{1}}], [eqn: i _{V _{1}}][eqn: )], [eqn: (][eqn: i_{ n _{ 2} }], [eqn: i_{ V _{ 2} }][eqn: )]…[eqn: right], [eqn: O] [eqn: =] [eqn: left{][eqn: (][eqn: o_{ n _{ 1} }], [eqn: o_{ n _{ 1} }][eqn: )], [eqn: (][eqn: o_{ n _{ 2} }], [eqn: o _{V _{2}}][eqn: )]…[eqn: right], [eqn: I T] [eqn: =] [eqn: I``` SMALLINTER O]I는 각각 입력 이벤트와 출력 이벤트, 그리고 내부 이벤트의 집합이다. fFSM 모델은 계층성, 병행성 그리고 변수 상태(variable state)를 지원한다. [eqn: X] [eqn: =] [eqn: left{][eqn: (][eqn: x _{n _{1}}], [eqn: x _{V _{1}}][eqn: )], [eqn: (][eqn: x _{n _{2}}], [eqn: x _{V _{2}}][eqn: )]…[eqn: right}]은 상태집합 이름과 각 상태집합이 가지는 실제의 유한 집합의 쌍으로 된 유한 집합이다. [eqn: V SUBSET X]는 변수 상태의 이름과 해당 값의 범위 집합으로 짝지어진 쌍의 유한 집합이다. [eqn: R] [eqn: SUBSETEQ] [eqn: left{][eqn: (][eqn: x_{ n}], [eqn: x _{v}][eqn: )] | [eqn: (][eqn: x _{n}], [eqn: x _{v}][eqn: )] [eqn: IN] [eqn: X], [eqn: x _{v}][eqn: IN][eqn: x _{V}][eqn: right}]은 초기 상태들의 집합이다. 모든 [eqn: (][eqn: x_{ n}], [eqn: x _{V}][eqn: )]에 대해서 유일한 [eqn: (][eqn: x_{ n}], [eqn: x _{V}][eqn: )][eqn: IN][eqn: R]을 갖는다. 전이는 가드 조건 [eqn: f ^{G}]이 만족할 때, 액션 [eqn: f ^{A}]을 수행하면서 현재 상태 [eqn: f ^{X`I}]로부터 다음 상태인 [eqn: f ^{XO}]상태로 진행된다. 따라서 전이 집합은 [eqn: F][eqn: SUBSETEQ][eqn: f ^{X`I}][eqn: TIMES][eqn: f ^{G}][eqn: TIMES][eqn: f ^{XO}][eqn: TIMES][eqn: f ^{A}] 이다. 가드 조건은 입력 이벤트와 변수상태의 조합으로 된 부울식이다. 액션은 출력 이벤트의 발생 혹은 내부 이벤트와 변수에 대한 값의 변경의 집합으로 표현된다. [eqn: f ^{X`I}][eqn: CUP][eqn: f ^{XO}][eqn: SUBSETEQ][eqn: left{][eqn: (][eqn: x_{ n}], [eqn: x _{V}][eqn: )] | [eqn: (][eqn: x_{ n}], [eqn: x _{V}][eqn: )][eqn: IN][eqn: X], [eqn: x_{ n}][eqn: IN][eqn: x _{V}][eqn: right}]전이의 출발상태와 도착상태의 집합이다. [eqn: f ^{G}][eqn: =][eqn: f][eqn: (][eqn: e _{n _{1}}], [eqn: e _{n _{2}}], …[eqn: )] [eqn: =] true or false, [eqn: (][eqn: e _{n _{k}}], [eqn: e _{V _{k}}][eqn: )][eqn: IN][eqn: I] [eqn: CUP][eqn: V]는 입력과 변수 상태로 구성된 부울 식이다. [eqn: f ^{A}][eqn: SUBSETEQ][eqn: left{][eqn: (][eqn: r _{n}], [eqn: f ^{R}][eqn: )] | [eqn: (][eqn: r _{n}], [eqn: r _{v}][eqn: )][eqn: IN][eqn: O][eqn: CUP][eqn: V], [eqn: f ^{R}][eqn: =] [eqn: f][eqn: (][eqn: e _{n _{1}}], [eqn: e _{n _{2}}], …[eqn: )][eqn: SUBSETEQ][eqn: r _{V}], [eqn: (][eqn: e _{n _{k}}], [eqn: e _{V _{k}}][eqn: )][eqn: IN][eqn: I] [eqn: CUP][eqn: V][eqn: right}]는 액션들 [eqn: (][eqn: r _{n}][eqn: =][eqn: f ^{R}][eqn: )]의 집합이다. 도착상태 [eqn: r _{n}]와 함수 [eqn: f ^{R}]. 함수는 입력 이벤트와 변수 상태로 구성된다[8].

(그림 1) fFSM 예제, reflex game

fFSM 모델은 다음과 같은 제약사항을 갖는다. 첫째, 변수 상태는 단지 원소(atomic) fFSM에서만 참조되고 갱신된다. 원소 fFSM은 변수 상태를 제외한 오직 하나의 상태 집합만을 갖는 것이다. 즉, |[eqn: X][eqn: -][eqn: V]|[eqn: =]1, 따라서 그림 1에서 원소 fFSM은 [eqn: s _{2}], [eqn: s _{3}], [eqn: s _{4}]가 된다. 둘째, 병행 fFSM들 간에는 계층간 전이를 허용하지 않는다. 셋째, 병행 fFSM 간의 통신은 단지 내부 이벤트에 의해서만 이루어진다. 그림 1의 fFSM 모델에서 입력 이벤트는 coin, ready, stop, time이 있고 마지막 이벤트는 시스템에 의해서 시간을 줄여 가는데 사용된다.

그림 1에 대한 fFSM 정의는 아래와 같다. fFSM의 동작은 우선 입력 이벤트에 의해서 트리거 된다. 그리고 가드조건이 만족될 때 전이가 발생된다. 만일 전이가 내부 이벤트를 발생시키면 그 내부 이벤트에 의해서 트리거 되는 전이는 더 이상 내부 이벤트가 없을 때까지 반복적으로 발생된다. 매 델타-지연 후에 존재하는 모든 이벤트는 삭제된다. 그리고 이전 델타-지연에서 새롭게 생성된 내부 이벤트들을 준비한다.

I = {(coin, {[eqn: epsilon]}), (ready, {[eqn: epsilon]}), (stop, {[eqn: epsilon]}), (time, {[eqn: epsilon]}), (timeout, {[eqn: epsilon]}), (error, {[eqn: epsilon]}), (exit, {[eqn: epsilon]}), (timeset, {0, …, 1000})}

O = {(timeout, {[eqn: epsilon]}), (error, {[eqn: epsilon]}), (exit, {[eqn: epsilon]}), (timeset, {0, …, 1000}), (game_on, {[eqn: epsilon]}), (waitGo, {[eqn: epsilon]}), (waitStop, {[eqn: epsilon]}), (ringBell, {[eqn: epsilon]}), (tilt, {[eqn: epsilon]}), (game_over, {[eqn: epsilon]})}

IT = {(timeout, {[eqn: epsilon]}), (error, {[eqn: epsilon]}), (exit, {[eqn: epsilon]}), (timeset, {0, …, 1000})}

X =  {([eqn: s _{1}], {GameOff, GameOn}), ([eqn: s _{2}], {wait, TimeInit}), ([eqn: s _{3}], {Ready, Go, Stop, End}), ([eqn: s _{4}], {Rand}), (remain, {0, …, 1000}), (randn, {1, …, 3})}

V =  {(remain, {0, …, 1000}), (randn, {1, …, 3})}

R =  {([eqn: s _{1}], GameOff), (s2,TimeInit), (s3, Ready), (s4, Rand), (remain, 0), (randn, 3)}

F =  {(([eqn: s _{1}], GameOff), (coin == [eqn: epsilon]), ([eqn: s _{1}], GameOn), {game_on=[eqn: epsilon], timeset=1000}), (([eqn: s _{1}], GameOn), (exit ==[eqn: epsilon]), ([eqn: s _{1}], GameOff), {ringBell=[eqn: epsilon], game_over=[eqn: epsilon]}), (([eqn: s _{1}], GameOn), (erro r==[eqn: epsilon]), ([eqn: s _{1}], GameOff), {tilt=[eqn: epsilon], game_over=[eqn: epsilon]}), …}

2.2 pFSM(parallel FSM)의 구문

fFSM의 단계의미를 정의하기 위해서, 우리는 fFSM의 각 FSM을 평탄화한 N 병행기계인 pFSM을 제안한다. 여기서 N은 fFSM에 포함된FSM의 수이다. pFSM의 I, O, IT 는 각각 입력 이벤트, 출력 이벤트, 내부 이벤트의 집합이다. fFSM과는 달리 이 세 개의 집합을서로 소인 집합으로 정의했다. [eqn: I] [eqn: CUP][eqn: O] [eqn: CUP][eqn: I T][eqn: =]{[eqn: e _{1}], ... , [eqn: e _{n}]}에 있는 각 이벤트 [eqn: e _{i}]는 도메인 [eqn: D _{i}]와 초기값 [eqn: d _{i}]로 구성되고, [eqn: val(e _{i} )]은 그 이벤트의 현재 값을 의미한다. 단순(Simple) FSM은 4개의 튜플 [eqn: (S,`s ^{0} ,`T,`scr)]로 정의 되는데, 여기서 [eqn: S]는 상태들의 집합이고 [eqn: s ^{0}]는 초기 상태이며, [eqn: T]는 전이들의 집합이다.

PeaCE에서 데이터 흐름 모델들은 fFSM에서 생성되는 외부 신호에 의해서 제어된다. 이러한 신호들은 해당 상태에 원소 명제의 집합으로 레이블 된다. 우리는 이러한 레이블을 스크립트(scripts)라고 부르고, Script는 fFSM 내에서 나타나는 모든 스크립트들의 집합을 나타낸다. 따라서, [eqn: scr:S` -> `2 ^{Script}] 는 각 상태에 스크립트를 레이블 하는 함수로 정의 된다.

정의 2 (parallel FSM) [eqn: pFSM] [eqn: =] [eqn: (][eqn: I], [eqn: O], [eqn: I`T], [eqn: M], [eqn: gamma], [eqn: V][eqn: )], [eqn: I], [eqn: O], [eqn: I`T] 이벤트들의 집합이다. [eqn: V] 전역변수의 집합이고, [eqn: v _{j}][eqn: IN][eqn: (][eqn: D _{j}], [eqn: d _{j}][eqn: )], [eqn: M][eqn: =]{[eqn: m _{1}], ..., [eqn: m _{n}]}는 단순 FSM의 집합이다. [eqn: SMALLSUM][eqn: =][eqn: union _{i=1} ^{n}][eqn: S _{i}]은 [eqn: M] 에 속한 모든 상태들의 집합이다. 계층 관계 [eqn: gamma] 는 상태를 그 상태가 포함하는 상태 기계들로 사상하는 함수이다: [eqn: gamma] :[eqn: SMALLSUM][eqn: ->][eqn: 2 ^{M}].

계층함수 [eqn: gamma] 는 다음의 세 가지 속성을 갖는다. 첫째, 유일한 루트 상태 기계를 갖는다. 둘째, 루트를 제외한 모든 상태 기계들은 정확하게 하나의 조상 상태를 갖는다. 셋째, 계층함수는 싸이클을 포함하지 않는다. [eqn: s`ub] : [eqn: SMALLSUM][eqn: ->][eqn: 2 ^{SMALLSUM }]일 때, [eqn: s`ub(s)][eqn: =]{[eqn: s']|[eqn: M _{i}][eqn: IN][eqn: gamma (s)][eqn: WEDGE][eqn: s'][eqn: IN][eqn: S _{i}]}는 어떤 상태에 포함된 하위 상태들을 돌려주는 함수이다. [eqn: s`ub ^{+}] 은 [eqn: s`ub] 의 추이 클로우져(transitive closure)이고 [eqn: s`ub ^{*}]는 [eqn: s`ub]의 반사적 추이 클로우져(reflexive transitive closure)이다.

정의 3 (simple FSM) [eqn: m _{i}] [eqn: =] [eqn: (][eqn: S _{i}], [eqn: s _{i} ^{0}], [eqn: T _{i}], [eqn: scr _{i}][eqn: )], [eqn: S _{i}] [eqn: =] [eqn: (][eqn: s _{i} ^{0}], [eqn: s _{i} ^{1}], ..., [eqn: s _{i} ^{n}][eqn: )]는 [eqn: m _{i}]의 유한 상태들의 집합 [eqn: s _{i} ^{0}]는 초기상태, [eqn: T _{i}]은 [eqn: m _{i}],의 전이들의 집합이고 전이 [eqn: t][eqn: IN][eqn: T _{i}][eqn: =][eqn: (][eqn: s], [eqn: g], [eqn: A], [eqn: s'][eqn: )]는 출발 상태, 도착 상태 [eqn: s], [eqn: s']와 부울식으로 표현되는 가드 조건 [eqn: g] 그리고 액션 집합 [eqn: A]로 구성된다. [eqn: scr _{i} :S _{i} ` -> `2 ^{Script}] 는 상태에 스크립트를 사상하는 함수이다.

변수와 이벤트를 포함하는 가드는 아래와 같이 간단한 구문으로 정의된다.

[eqn: G::=true`|`` LNOT G``|`G _{1} WEDGE G _{2} ``|`e<E`xp``|`e=E`xp``|`v<E`xp``|`v=E`xp]

[eqn: E`xp`::=`n``|`v``|`E`xp _{1} BULLET E`xp _{2} `],

여기서 [eqn: n] 은 정수를 대표하고, [eqn: v IN V] 는 전역변수이며, [eqn: BULLET][eqn: IN]{[eqn: +], [eqn: -] , [eqn: TIMES] , [eqn: /]}는 이진 연산자를 대표한다. 전이 [eqn: t][eqn: =][eqn: (][eqn: s], [eqn: g], [eqn: A], [eqn: s'][eqn: )]의 한 요소를 선택하기 위해서, 추출 함수가 사용 된다 :

[eqn: source(t)][eqn: =][eqn: s], [eqn: target(t)][eqn: =][eqn: s'], [eqn: guard(t)][eqn: =][eqn: g], , [eqn: action(t)][eqn: =][eqn: A].

또한, 액션의 집합 [eqn: A]의 각 원소 [eqn: a IN A]들은 아래와 같이 변수의 값 배정이나출력 이벤트의 방출로 구성 된다:

[eqn: a][eqn: ::=][eqn: v][eqn: :=][eqn: E`xp]|[eqn: e][eqn: :=][eqn: E`xp].

액션에 대해서도 다음과 같은 세 개의 추출 함수가 쓰인다, 이들은 각각변수의 갱신, 출력 이벤트의 방출, 내부 이벤트의 생성에 관한 부분을 추출할 때 사용된다.

[eqn: update(A)=]{[eqn: v:=E`xp``|` EXIST v IN V.(v:=E`xp) IN A]}

[eqn: output(A)=]{[eqn: e:=E`xp``|` EXIST e IN O.(e:=E`xp) IN A]}

[eqn: signal(A)=]{[eqn: e:=E`xp``|` EXIST e IN I`T.(e:=E`xp) IN A]}

그림 2는 그림 1에 해당하는 pFSM이다. 그리고 아래의 예는 그림 2에 대한 pFSM 정의를일부 나타낸 것이다.

(그림 2) 평탄화된 상태기계들

I = {coin, ready, stop, time}, O = {game_on, waitGo, waitStop, ringBell, tilt, game_over}

IT = {timeset, timeout, error, exit}, V = {randn, remain}

M = {[eqn: m _{1}], [eqn: m _{2}], [eqn: m _{3}], [eqn: m _{4}]}, [eqn: gamma]([eqn: m _{1}]) = {[eqn: m _{3}], [eqn: m _{4}]}, [eqn: gamma]([eqn: m _{2}]) =  [eqn: gamma]([eqn: m _{3}]) = [eqn: gamma]([eqn: m _{4}]) = [eqn: ODIV],

[eqn: m _{1}] [eqn: =] [eqn: (][eqn: S _{1}], [eqn: s _{1} ^{0}], [eqn: T _{1}], [eqn: scr _{1}][eqn: )], [eqn: s _{1}] = {GameOff, GameOn}, = GameOff,

[eqn: T _{1}] = {(GameOff, coin = 1, {game_on = 1, timeset = 1000}, GameOn), (GameOn, exit = 1, {game_over = 1, ringBell = 1}, GameOff), (GameOn, error = 1, {game_over = 1, tilt = 1}, GameOff}, scr1 = [eqn: ODIV]

3. pFSM의 의미

fFSM 모델의 정형 분석

프로그래밍언어논문지 제 권 제 호 (    . )

fFSM의 단계 의미는 입력 이벤트나 내부 이벤트에 의해서 모델의 형상(configuration)이 변해가는 과정과 동시에 액션의 수행을 묘사하는 것인데, 여기서 액션은 출력 이벤트의 방출과 전역변수의 갱신 그리고 또 다른 내부 이벤트의 생성으로 구성된다.

정의 4 (형상) [eqn: DELTA]는 pFSM 모델의 전제 형상을 나타낸다, pFSM의 각 [eqn: m _{i}]i 에 대해서, 형상 집합의 정형적 정의는 [eqn: DELTA][eqn: =]{{[eqn: s _{1}], ..., [eqn: s _{n}]} |[eqn: EXIST s _{i}][eqn: IN][eqn: S _{i}],[eqn: 0<i<n]}가 된다. [eqn: delta _{0} IN DELTA], [eqn: delta _{0}][eqn: =]{[eqn: s _{1} ^{0}], ..., [eqn: s _{n} ^{0}]} 는 초기 형상이다.

정의 5 (활성화된 상태) 상태 [eqn: s]가 형상에서 활성화 되었다는 것은 다음과 같이 정의될 수 있다:

[eqn: delta MODELS s`] iff [eqn: FORALL s prime IN SMALLSUM .s IN s`ub ^{*} (s prime )` RARROW `s prime IN ` delta].

정의 6 (만족성) 어떤 전이가 활성화된 전이(enabled transition)인지를 결정하기 위해, 이벤트의 집합[eqn: E SUBSETEQ 2 ^{I} ` CUP `2 ^{I`T}]과 현재의 형상 [eqn: delta]가 주어졌을 때, 형상 [eqn: delta]와 이벤트 [eqn: E]는 가드 [eqn: g]를 만족한다는 것, [eqn: LEFT < delta ,`E RIGHT > MODELS guard(t)]을 아래와 같이 귀납적으로 정의한다.

[eqn: LEFT < delta ,`E RIGHT > MODELS true]     iff  [eqn: true]

[eqn: LEFT < delta ,`E RIGHT > MODELS ` LNOT G]     iff  [eqn: LEFT < delta ,`E RIGHT > MODELS G]

[eqn: LEFT < delta ,`E RIGHT > MODELS `G _{1} ` WEDGE G _{2}]  iff  [eqn: LEFT < delta ,`E RIGHT > MODELS G _{1} ``and`` LEFT < delta ,`E RIGHT > MODELS G _{2}]

[eqn: LEFT < delta ,`E RIGHT > MODELS `e<E`xp]  iff  [eqn: e IN E```and```val(e)`<`val(E`xp)]

[eqn: LEFT < delta ,`E RIGHT > MODELS `e=E`xp]  iff  [eqn: e IN E```and```val(e)`=`val(E`xp)]

[eqn: LEFT < delta ,`E RIGHT > MODELS `v<E`xp]  iff  [eqn: val(v)`<`val(E`xp)]

[eqn: LEFT < delta ,`E RIGHT > MODELS `v=E`xp]  iff  [eqn: val(v)`=`val(E`xp)]

여기서 [eqn: val(n)=n] 이고, [eqn: val(e)]은 이벤트 [eqn: e]의 현재 값을 나타내며, [eqn: val(v)]는 변수 [eqn: v]의 현재 값을 나타낸다.

[eqn: val(E`xp _{1} BULLET E`xp _{2} )][eqn: =][eqn: val(E`xp _{1} )][eqn: BULLET][eqn: val(E`xp _{2} )].

정의 7 (활성화된 전이) 활성화된 상태와 만족성 관계(satisfiability relation)의 정의에 의해서, 각 활성화된 상태에 대해서 활성화된 전이의 집합을 다음과 같이 정의한다.

[eqn: LEFT . EF```=` LEFT { t`|` FORALL i IN RIGHT . LEFT { 1,`...,`n RIGHT } .t IN T _{i} RIGHT .]

[eqn: LEFT . WEDGE LEFT < delta ,`E RIGHT > MODELS guard(t) WEDGE delta MODELS source(t) RIGHT }]

정의 8 (실행 전이) 실행 전이(executable transition)들의 집합은 충돌이 없는 가장 큰 전이들의 집합이고 반드시 모든 단순 FSM에서 최대 하나의 전이가 포함된다. fFSM 모델은 계층간 전이를 허용하지 않기 때문에, 충돌은 단지 우선순위를 비교할 수 있는 두 전이 사이에서만 발생한다.

[eqn: XT``=`left{t IN ET``|` LNOT EXIST t prime IN ET.source(t)]

[eqn: IN s ub ^{+} (source(t prime )) right}],

[eqn: FORALL m _{i} IN M.`|XT` SMALLINTER T _{i} ``|` LEQ 1]

정의 9 (LKS) pFSM 의 단계의미는 전이가 레이블 되는 크립키 구조인 LKS(Labeled Kripke Structure)로 정의된다. [eqn: LKS][eqn: =][eqn: (][eqn: Q], [eqn: q _{0}], [eqn: R], [eqn: L][eqn: )] 에서 [eqn: Q][eqn: =]{[eqn: q _{0}], ..., [eqn: q _{n}]}는 [eqn: LKS]의 유한 상태 집합, [eqn: q _{0}][eqn: =][eqn: (][eqn: delta _{0}], [eqn: EMPTYSET], [eqn: c _{0}][eqn: )]는 초기상태, [eqn: R][eqn: SUBSET][eqn: Q][eqn: TIMES][eqn: 2 ^{Act}][eqn: TIMES][eqn: Q]는 액션으로 레이블 된 전이관계, [eqn: L]:[eqn: Q][eqn: ->][eqn: 2 ^{Script}]는 레이블 함수로써 [eqn: L(q _{i} )][eqn: =][eqn: union _{delta _{i} MODELS s} ^{} scr(s)] 이다.

정의 10 (마이크로 스텝)

[eqn: (][eqn: delta], [eqn: E], [eqn: c][eqn: )] [eqn: REL -> {``````````Act``````````} {}][eqn: (][eqn: delta '], [eqn: E'], [eqn: c'][eqn: )]

현재 형상 [eqn: delta]와 이벤트의 집합 [eqn: E]가 주어졌을 때, 마이크로 스텝은 [eqn: LKS] 상에서 다음과 같이 정의 된다:

[eqn: delta prime = LEFT { s prime `|` FORALL s IN delta `. EXIST t IN XT`. RIGHT .]

[eqn: (s=source(t)`` RARROW `s'=target(t))]

[eqn: LOR (s IN s`ub ^{+} (source(t))`` RARROW `s prime =reset(s))]

[eqn: LEFT. LOR (s NOTIN s`ub ^{*} (source(t))`` RARROW `s prime =s) RIGHT }]

여기서 [eqn: reset(s)=][eqn: s _{i} ^{0}], [eqn: s IN s`ub(s '' )][eqn: WEDGE m _{i} IN gamma (s'')]

[eqn: WEDGE s IN S _{i}]이다.

[eqn: E prime = union _{FORALL t IN XT} ^{} signal(action(t))], [eqn: c'=L(q')],

[eqn: Act= union _{FORALL t IN XT} ^{} output(action(t))]

[eqn: CUP union _{FORALL t IN XT} ^{} update(action(t))]

정의 11 (매크로 스텝) pFSM의 단계 의미는 실행(execution) 로 정의된다. 하나의 입력 이벤트 집합과 연속해서 발생되는 내부 이벤트들의 집합은 더 이상 내부 이벤트가 없을 때까지 전이를 발생시킨다. 매 마이크로스텝 후에, 델타-지연에 의해서 이전의 이벤트들은 모두 소멸된다. 아래의 정의에서, [eqn: k>1]는 [eqn: E _{i,k}]가 [eqn: EMPTYSET]이 되게 하는 첫 번째 [eqn: k]를 의미한다. 그리고 [eqn: Exe _{i} = union _{FORALL 0<j<k} ^{} Act] 는 매크로 스텝 동안에 이뤄지는 액션들의 집합을 의미한다.

[eqn: ( delta _{i} ,`E _{i} ,`c)` REL -> {``Exe _{i} ``} {} `( delta prime _{i+1} ,`E prime _{i+1} ,`c prime _{i+1} )]  iff

[eqn: ( delta _{i,1} ,`E _{i,1} ,`c _{i,1} )` REL -> {`Act _{1} `} {} ``...` REL -> {`Act _{k-1} `} {} `( delta prime _{i,k} ,` EMPTYSET ,`c prime _{i,k} ).]

마이크로 스텝은 입력 또는 내부 이벤트에 의해서 한번 전이되는 과정을 말한다. 매크로 스텝은 입력 또는 연속해서 발생되는 내부 이벤트들에 의해서 추가적인 입력 이벤트 없이 더 이상 전이가 없을 때까지의 이루어지는 모든 전이과정을 의미한다. 따라서 매크로 스텝은 마이크로 스텝들의 연속이다. 그림 3은 입력 이벤트 coin이 발생했을 때, 시스템이 초기형상 {GameOff, TimeInit, Ready, Rand}로부터 다음 형상 {GameOn, wait, Ready, Rand}로 움직여 나가는 모습을 보여준다.

(그림 3) 마이크로 스텝(a)과 매크로 스텝(b)

(그림 4) 동기화 가정

4. fFSM의 CTL 모델체킹

4.1. 속성 표현

앞 장에서 정의된 단계의미를 이용하면 모델의 주요 오류들을 디버깅할 수 있는데, 우리는 PeaCE 도구에서 정형 모델 분석을 위해 아래와 같은 속성을 자동으로 검사할 수 있는 검증 도구를 개발했다.

(1) No race condition, No ambiguous transitions, No circular transitions

(2) No unused components, No unreachable guards, No deadlocks

이 장에서는 이러한 정형 분석을 모델체킹을 이용해서 검증하는 과정을 다룬다. 먼저 만족해야 하는 속성을 CTL식으로 나타내는 방법을 살펴본 후에 모델을 대표적인 CTL 모델체커인 SMV의 입력언어로 변화하는 방법에 대해서 설명한다. CTL 논리의 구문과 의미 및 SMV 입력언어에 대해서는 [9]를 따른다.

속성의 정의와 정형화를 쉽게 하기 위해서 먼저 매크로 스텝과 마이크로 스텝, 그리고 동기화 가정(synchrony hypothesis)에 대해서 살펴보자. 아래 그림 4는 환경에 변화에 따라 동작하는 시스템의 행위를 스텝을 기준으로 나타낸 것이다. 환경의 변화는 시스템에 대한 외부의 자극이라고도 생각해 볼 수 있다. 즉 외부의 자극과 자극 사이에 시스템의 동작을 매크로 스텝이라고 하고, 한 매크로 스텝 동안에 시스템 내부 동작을 마이크로 스텝이라고 한다. 환경 변화 후 시스템의 내부 동작이 모두 완료되는 시점을 안정한(stable) 상태라고 한다. 여기서 동기화 가정이란 매크로 스텝은 외부의 변화보다 훨씬 빠르다는 가정이다. 즉 환경 변화의 속도보다 시스템의 처리 속도가 비교할 수 없을 만큼 빠르다는 것이다.

Race condition은 한 매크로 스텝 안에서 변수 상태 값이 두 번 이상 변경되거나, 출력 이벤트가 두 번 이상 방출될 때로 정의된다. 즉 한 매크로 동안에는 그 값이 일정해야 한다는 것이다. 따라서 “시스템이 안정하지 않은 상태에서 어떤 변수나 이벤트가 한번 변경되거나 방출되었다면 시스템이 다시 안정화 될 때까지 해당 변수나 이벤트의 변경과 방출은 허용되지 않는다.”라고 표현할 수 있다. [eqn: change(v)]를 시스템 내부의 변수 [eqn: v]의 변경 여부를 식별하는 함수라고 하고, [eqn: emit(o)]는 출력 이벤트 [eqn: o]의 방출이라고 정의하자. CTL은 명제논리에 기반 하기 때문에 변수 [eqn: v][eqn: IN][eqn: V] 에 대해서 각각 검사해야 하고 출력 이벤트 [eqn: o]에 대해서도 같은 방식이 적용된다. 이제 Race condition을 CTL식으로 나타내면 다음과 같다. 여기서 안정화된 상태를 의미하는 stable은 내부 이벤트가 발생되지 않는 상태로 정의할 수 있으며, 다음 절에서 설명될 것이다.

[eqn: AG``((change(v) WEDGE `` LNOT stable)``]

[eqn: RARROW ``AX```A[` LNOT change(v)` CUP `stable])]

[eqn: AG((emit(o)` WEDGE ` LNOT stable)]

[eqn: RARROW ``AX```A[` LNOT emit(o)` CUP `stable])]

애매한 전이(Ambiguous transition)는 하나의 상태에서 두 개 이상의 전이가 동시에 발생하는 상황을 의미한다. 이것은 전이의 쌍을 검사함으로써 알 수 있다. 만일 상태 [eqn: s]에서 발생되는 전이 집합이 {[eqn: t _{1}], [eqn: t _{2}], [eqn: t _{3}]} 라고 한다면 상태 [eqn: s]에 대한 애매한 전이의 존재 여부는 아래와 같이 CTL 식으로 나타낼 수 있다.

[eqn: AG`` LNOT ((t _{1} WEDGE t _{2} ) LOR (t _{2} WEDGE t _{3} ) LOR (t _{1} WEDGE t _{3} ))]

순환 전이(Circular transitions)는 마이크로 스텝이 계속 되는 것을 의미한다. 즉, 외부 이벤트에 의해서 전이가 발생한 후 계속되는 내부 이벤트에 의해서 시스템이 안정화되지 않는 경우이다. 이를 CTL 식으로 표현하면 아래와 같다.

[eqn: AG( LNOT stable` RARROW `A[` LNOT stable` CUP `stable])]

위의 세 종류 외에도 데드락(Deadlock)과, 도달 불가능한 상태 분석과 발생되지 않는 전이, 사용되지 않는 컴포넌트에 대한 조사를 할 수 있다. 먼저 사용되지 않는 컴포넌트는 쉽게 표현된다. 여기서 컴포넌트란 변수가 될 수도 있고 이벤트가 될 수도 있다. 그러나 변수 [eqn: v]와 내부 이벤트 [eqn: e], 출력 이벤트 [eqn: o]에 대해서 [eqn: EF`] [eqn: omit(o)], [eqn: EF] [eqn: occur(o)] 또는 [eqn: EF] [eqn: change(v)] 형태의 식으로 간단히 검사할 수 있다. 여기서  [eqn: occur(o)]는 내부 이벤트의 발생을 의미한다. 전이 발생 여부는 전이 [eqn: t]의 출발상태 [eqn: source]와 도착상태 [eqn: target]이 있을 때, [eqn: EF] [eqn: (][eqn: source][eqn: WEDGE][eqn: EX] [eqn: target][eqn: )]로 표현 될 수 있다.

데드락은 모든 전이가 더 이상 활성화 되지 않는 상태가 영원히 지속됨으로 표현할 수 있다. 즉, fFSM의 모든 전이들의 집합을 [eqn: fT] [eqn: =] {[eqn: t _{1}], …, [eqn: t _{n}]}라고 할 때, 다음과 같이 CTL식으로 표현할 수 있다.

[eqn: LNOT `EF```AG``` LNOT `(t _{1} ```...```t _{n} )]

[eqn: Deadlock(fT)] [eqn: =] [eqn: LNOT union _{FORALL t IN fT} ^{{} _{}} ```t] 라고 정의 하면 위 식은 [eqn: EF] [eqn: AG] [eqn: Deadlock(fT)]로 대신 쓸 수 있다. 데드락은 전체 시스템에 해당하는 것과 일부 시스템에 해당하는 것으로 구분할 수 있다. 전자를 전역(Global) 데드락이라고 하고 후자를 지역(Local) 데드락이라고 한다. 지역 데드락은 마치 라이브 락(Livelock)과 같아서 전체 시스템 관점으로 보면 동작하는 것처럼 보이지만 시스템의 내부 모듈이 블록 되어서 향후 전혀 동작하지 않는 경우이다. 단순 FSM의 집합을 {[eqn: M _{1}], …, [eqn: M _{n}]}이라고 하고 각 모듈에 대한 전이 집합을 {[eqn: T _{1}], …, [eqn: T _{n}]}라고 한다면, 지역 데드락에 대한 식은 [eqn: LNOT][eqn: EF][eqn: AG] [eqn: Deadlock(T _{1} )][eqn: LOR]…[eqn: LOR][eqn: Deadlock(T _{n} )]으로 표현될 수 있다. 이때 [eqn: Deadlock(T _{i} )]는 단순 FSM의 집합에 속하는 원소 [eqn: M _{i}]의 데드락을 나타내며 전역 데드락을 다시 정의하면 [eqn: LNOT][eqn: EF][eqn: AG] [eqn: Deadlock(T _{1} )][eqn: WEDGE]…[eqn: WEDGE][eqn: Deadlock(T _{n} )]가 된다.

마지막으로 unreachable guards의 존재 여부를 분석할 때, 식 [eqn: EF] [eqn: t]를 적용할 수 있다. 여기서 [eqn: t]는 모델의 전이이다. 즉 “가드 조건에 도달하는가?” 하는 문제는 그 가드가 만족될 때, 발생되는 전이를 찾는 문제로 생각할 수 있고, 전이는 상태의 쌍으로 표현될 수 있다.

4.2 SMV 입력언어로 변환

모델 체킹을 하기 위해서 상태도를 모델 체커의 입력언어로 모델을 변환하는 연구는 지금껏 많이 수행되어왔다. 우리는 fFSM의 모델 체킹을 위해서 Chan[10]과Clarke[11]의 방식에서 많은 힌트를 얻었다. 2장에서 설명한 것과 같이 fFSM의 의미를 다루기 위해 우리는 N개의 머신으로 계층을 평탄화한 pFSM 정의했다. SMV의 변수들은 모두 병렬적으로 동작하므로 pFSM의 머신과 상태들은SMV의 변수와 변수 값으로 자연스럽게 변환할 수 있다.

변환규칙 1 (머신과 상태) [eqn: pFSM] [eqn: =] [eqn: (][eqn: I], [eqn: O], [eqn: I`T], [eqn: M], [eqn: gamma], [eqn: V][eqn: )] 일 때, [eqn: M]에 속한 머신 [eqn: m _{i}] [eqn: =] [eqn: (][eqn: S _{i}], [eqn: s _{i} ^{0}], [eqn: T], [eqn: scr _{i}][eqn: )]에 대해서 해당 상태들은 [eqn: VAR``m _{i} ``:`S _{i}]로 변환된다.

VAR

Machine1 : {GameOff, GameOn};

Machine2 : {Timeinit, Wait};

변환규칙 2 (전이)전이는 정의 7의 활성화된 전이 조건 [eqn: LEFT < delta ,E RIGHT >][eqn: MODELS][eqn: guard(t)] [eqn: WEDGE] [eqn: delta][eqn: MODELS][eqn: source(t)]에 의거하여 SMV로 변환하다. 즉,  [eqn: m _{i}] [eqn: =] [eqn: (][eqn: S _{i}], [eqn: s _{i} ^{0}], [eqn: T], [eqn: scr _{i}][eqn: )]와 [eqn: t IN T _{i}]에 대해서 어떤 상태를 포함하는 상위 상태들을 돌려주는 함수가 [eqn: up(s)] = {[eqn: s prime] | [eqn: M _{i}][eqn: IN][eqn: gamma (s prime )][eqn: WEDGE][eqn: s IN S _{i}]} 는 이고, [eqn: up ^{*}]는 [eqn: up]의 반사적 추이 클로우져일 때, 각각의 전이들은 [eqn: DEFINE] [eqn: m _{i}]_[eqn: t] [eqn: :=] [eqn: up ^{*}][eqn: (][eqn: source(t)][eqn: )]&[eqn: guard(t)][eqn: )]로 변환된다.

DEFINE

Machine1_t1 := Machine1 = GameOn & error=1;

Machine1_t2 := Machine1 = GameOff & coin=1;

Machine1_t3 := Machine1 = GameOn & exit=1;

ASSIGN

init(Machine1) := GameOff;

next(Machine1) :=

case

Machine1_t1 : GameOff;

Machine1_t2 : GameOn;

Machine1_t3 : GameOff;

1 : Machine1;

esac;

변환규칙 3 (동기화 가정) 동기화 가정을 SMV에서 표현하기 위해, 그림 4에서 설명한 안정한 상태를 의미하는 특별한 이진 변수 [eqn: stable]을 추가한다. 안정한 상태는 내부 이벤트 {[eqn: i`nternal _{1}], …, [eqn: i`nternal _{l}]}가 발생하지 않는 상태로 간단히 정의할 수 있지만, 우리는 생성된 반례의 가독성을 높이기 위해서 입력 이벤트 {[eqn: input _{1}], …, [eqn: input _{m}]} 와 다중 값을 갖는 내부이벤트 {[eqn: valued _{1}], …, [eqn: valued _{n}]}를 함께 사용해서 변환한다.

VAR

stable : boolean;

ASSIGN

init(stable) := 1;

next(stable) :=

case

!([eqn: valued _{1}]= next([eqn: valued _{1}])) : 0;

!([eqn: valued _{n}]= next([eqn: valued _{n}])) : 0;

next([eqn: input _{1}]) | … | next([eqn: input _{m}]) : 0;

([eqn: i`nternal _{1}]=0) & … & ([eqn: i`nternal _{l}]=0) : 1;

1 : 0;

esac

변환규칙 4 (입력 이벤트) 초기값이 [eqn: d]인 입력 이벤트 [eqn: e]의 도메인 [eqn: D]이고 도메인의 최소값과 최대값이 각각 [eqn: min _{e}], [eqn: max _{e}]일 때, 다음과 같이 변환된다.

ASSIGN

init([eqn: e]) := [eqn: d]

next([eqn: e]) :=

case

stable : [eqn: min _{e}] .. [eqn: max _{e}]

1 : 0;

esac;

변환규칙 5 (출력 이벤트) 어떤 전이 [eqn: t][eqn: =][eqn: (][eqn: s], [eqn: g], [eqn: A], [eqn: s prime][eqn: )]이고, [eqn: action(t)][eqn: =][eqn: A]일 때, 초기값 [eqn: d]를 갖는 출력 이벤트 [eqn: e]에 대해서 [eqn: output(A)][eqn: =]{[eqn: e][eqn: :=][eqn: E`xp]|[eqn: EXIST e][eqn: IN][eqn: O].[eqn: (][eqn: e][eqn: :=][eqn: E`xp][eqn: )][eqn: IN][eqn: A]}을 만족하는 모든 전이 집합 {[eqn: t _{1}], …, [eqn: t _{n}]}과 각 식의 집합 {[eqn: E`xp _{1}], …, [eqn: E`xp _{n}]} 대해서 다음과 같이 변환한다.

ASSIGN

init([eqn: e]) := [eqn: d]

next([eqn: e]) :=

case

[eqn: t _{1}] : [eqn: E`xp _{1}]

[eqn: t _{n}] : [eqn: E`xp _{n}]

1 : 0;

esac;

변환규칙 6 (내부 이벤트) 어떤 전이[eqn: t][eqn: =][eqn: (][eqn: s], [eqn: g], [eqn: A], [eqn: s'][eqn: )]이고, [eqn: action(t)][eqn: =][eqn: A] 일 때, 초기값 [eqn: d]를 갖는 내부 이벤트 [eqn: e]에 대해서 [eqn: signal(A)][eqn: =]{[eqn: e][eqn: :=][eqn: E`xp]|[eqn: EXIST e][eqn: IN][eqn: I`T].[eqn: (][eqn: e][eqn: :=][eqn: E`xp][eqn: )][eqn: IN][eqn: A]}을 만족하는 모든 전이 집합 {[eqn: t _{1}], …, [eqn: t_{ n}]}과 각 식의 집합 {[eqn: E`xp _{1}], …, [eqn: E`xp _{n}]} 대해서 다음과 같이 변환한다.

ASSIGN

init([eqn: e]) := [eqn: d]

next([eqn: e]) :=

case

[eqn: t _{1}] : [eqn: E`xp _{1}]

[eqn: t _{n}] : [eqn: E`xp _{n}]

1 : 0

esac;

변환규칙 7 (변수) 어떤 전이[eqn: t][eqn: =][eqn: (][eqn: s], [eqn: g], [eqn: A], [eqn: s'][eqn: )]이고, [eqn: action(t)][eqn: =][eqn: A] 일 때, 초기값 [eqn: d]를 갖는 변수 [eqn: v]에 대해서 [eqn: update(A)][eqn: =]{[eqn: v][eqn: :=][eqn: E`xp]|[eqn: EXIST v][eqn: IN][eqn: V].[eqn: (][eqn: v][eqn: :=][eqn: E`xp][eqn: )][eqn: IN][eqn: A]}을 만족하는 모든 전이 집합 {[eqn: t _{1}], …, [eqn: t _{n}]}과 각 식의 집합 {[eqn: E`xp _{1}], …, [eqn: E`xp _{n}]} 대해서 다음과 같이 변환한다.

ASSIGN

init([eqn: v]) := [eqn: d]

next([eqn: v]) :=

case

[eqn: t _{1}] : [eqn: E`xp _{1}]

[eqn: t _{n}] : [eqn: E`xp _{n}]

1 : [eqn: v]

esac;

(그림 5) 시뮬레이션으로 결합 조건 위반 검출

이벤트의 변환은 델타-지연을 고려해서 전이가 발생되지 않으면 0으로 값을 되돌리도록 했고, 변수에 대한 변환은 지속적으로 값이 유지되도록 했다. 먼저 fFSM을 N 병행기계로 재 정의한 후에 SMV로 변환했기 때문에 계층성을 크게 고려하지 않고 비교적 간단히 변환할 수 있었다.

4.3 fFSM의 정형 분석

버그 검출의 예로써 Race Condition 위반의 예를 생각해 보자. 만일 현재의 형상이 {GameOn, Wait, Ready, Rand} 이고, 발생된 이벤트가 각각 ready 와 time일 때, 그리고 변수 상태 remain 의 값이 0일 때, 드문 경우이기는 하지만, 출력 이벤트와 변수 상태의 값이 한 실행 동안 지속되어야 한다는 제약사항을 위반하게 된다. 우리는 fFSM 모델에 대한 버그 검출을 위해 이 논문에서 제안한 단계의미를 적용해서 우선 시뮬레이터를 구현하였다. 아래 그림 5는 시뮬레이터를 이용해서 Race Condition 위반을 검출하는 과정을 보여준다. STEP[0]은 시스템이 초기 형상으로 초기화 되어 있음을 나타낸다. STEP[1]은 coin 이벤트가 발생된 후, 내부 이벤트 timeset이 연속해서 발생된 것을 나타낸다. 이때의 형상이 {GameOn, Wait, Ready, Rand}이고 ready 와 time 이벤트가 동시에 발생하면 한 매크로 스텝 내에서 remain 값이 두 번 이상 변경되므로 시뮬레이터는 Race Condition 위반을 검출하게 된다.

사용자가 손쉽게 버그를 잡도록 돕는데 시뮬레이션이 빈번히 사용되지만, 시뮬레이션만으로는 중요한 버그를 철저한 정형 분석은 하기 어렵다. 따라서 모델체킹 기법으로 시스템의 행위를 철저하게 검사하는 검증 활동이 필요하다. 우리는 시뮬레이션 툴에 모델체킹이 가능하도록 하기 위해, 3장에서 설명한 것과 같이 fFSM 모델을 SMV 입력 언어로 바꾸고, 사용자에 의해 검증할 속성을 선택하도록 한 후, 속성을 CTL 논리로 변환하여 검증을 수행하도록 했다. 내부 검증기로는 Cadence SMV를 사용했다. 그림 6은 앞 절에서 시뮬레이션을 이용해서 검출했던 Race Condition 위반 사례를 모델체킹을 이용해서 검출한 것이다. 이 버그를 검출하기 위해 모델체킹 시간은 6초, BDD 노드는 456022개, 메모리는 15Mb를 사용했다. 비록 작은 모델이기는 하지만, 비교적 빠른 시간 안에 전체 상태공간을 탐색하게 된다. 특히 실제 시뮬레이션으로 같은 버그를 찾아내는 과정은 이보다 훨씬 더 많은 노력과 시간이 들어간다. 우리는 6가지 built-in 속성뿐 아니라 사용자에 의해서 직접 CTL 논리로 속성을 기술할 수 있도록 하였다.

(그림 6) 모델체킹을 이용한 Race Condition 위반 검출

5. 결론과 향후 연구

복잡한 임베디드 시스템을 설계하는 방법으로, 하드웨어/소프트웨어 통합설계가 제품의 생산성을 높일 새로운 방법론으로 주목 받고 있다. PeaCE[1]는 하드웨어/소프트웨어 통합 설계 프레임워크로써 데이터 흐름과 제어 흐름을 표현하는 모델을 가지고 있다. fFSM는 PeaCE의 제어 흐름을 표현하는 모델이다. 그러나 정형 의미의 부재로 명세를 정형 분석하는데 어려움이 있었다.

본 논문에서는, fFSM 모델의 단계의미를 병행기계인 pFSM을 이용해서 정의하였다. 그런 후 그 단계의미를 기반 하여 시뮬레이션과 모델체킹이 가능한 검증 도구를 개발했다. 그 결과 해당 버그를 정형적으로 분석할 수 있게 되었고, 사용자들은 푸쉬버튼 방식으로 속성들을 선택할 수 있기 때문에 보다 쉽게 제어흐름 모델의 에러를 검사할 수 있도록 하였다. 현재 우리는 본 논문에서 정의된 fFSM의 단계 의미를 기반으로 fFSM 전용의 모델체커를 개발하고 있다. 이를 위해 효율적인 추상화 방법을 연구하고 있다. 뿐만 아니라 앞으로는 제어흐름 모델에 대한 정형 의미와 두 모델간의 의미 통합에 관한 연구를 진행할 것이다.

참고문헌

[1] D. Kim, S. Ha, "Static Analysis and Automatic Code Synthesis of flexible FSM Model," ASP-DAC 2005 Jan 18-21, 2005

[2] D. Harel, A. Naamad, "The STATEMATE semantics of statecharts", ACM Transactions on Software Engineering Methodology, 5(4), October 1996.

[3] iLogix: http://www.ilogix.com/.

[4] http://ptolemy.eecs.berkeley.edu/

[5] E. Mikk, Y. Lakhnech, M. Siegel, "Hierarchical automata as model for statecharts,"LNCS Vol. 1345, Proceedings of the 3rd ACSC, pp. 181-196, 1997.

[6] J. Lind-Nielsen, H. R. Andersen, H. Hulgaard, G. Behrmann, K. J. Kristoffersen, K. G. Larsen, "Verification of Large State/Event Systems Using Compositionality and Dependency Analysis," FMSD, pp. 5-23, 2001.

[7] IAR: http://www.iar.com/products/vs/

[8] D. Kim, "System-Level Specification and Cosimulation for Multimedia Embedded Systems," Ph.D. Dissertation, Computer Science Department, Seoul National University, 2004.

[9] E. M. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999.

[10] W. Chan, "Symbolic Model checking for Large software Specification", Dissertation, Computer Science and Engineering at University of Washington, pp. 13-32, 1999.

[11] E. M. Clarke, W. Heinle, "Modular translation of Statecharts to SMV", Technical Report CMU-CS-00-XXX, CMU School of Computer Science, August 2000.

[12] J. B. Lind-Nielsen, "Verification of Large State/Event Systems," Ph.D. Dissertation, Department of Information Technology, Technical University of Denmark, 2000.

박 사 천

2001년 경기대학교 전자계산학과 졸업(학사)

2001년~ 2003년 경기대학교 전자계산학과 졸업(석사)

2004년 ~ 현재 경기대학교 전자계산학과 박사과정

<관심분야> 모델 체킹 , 정형기법, 소프트웨어 공학

권 기 현

1985년 경기대학교 전자계산학과 졸업(학사)

1987년 중앙대학교 전자계산학과 졸업(이학석사)

1991년 중앙대학교 전자계산학과 졸업(공학박사)

1998년~1999년 독일드레스덴 대학 전자계산학과 방문교수

1999년~2000년: 미국 카네기 멜론 대학 전자계산            학과 방문교수

1991년~현재: 경기대학교 정보과학부 교수

<관심분야> 소프트웨어 모델링, 소프트웨어 분석, 정형 기법등