공정안전검색을 위한 반증예제 생성 알고리듬

고 세 준, 문  일

연세대학교 화학공학과

Witness Generation Algorithm

for the Verification of Chemical Process Safety

Se-Jun Goh and Il Moon

Department of Chemical Engineering, Yonsei University

서론

SMV(Symbolic Model Verifier)는 전산학과에서 최초로 개발된 것으로[4], 원래는 논리식의 참과 거짓을 검증하는 검증기로서 개발되었다. 하지만 SMV의 검증효과가 뛰어남에 따라 이를 다른 분야에 적용하려는 시도가 계속되었고, 화공 분야-특히 공정시스템 분야-에서 공정의 안전 검색을 위한 논리식의 검증에 SMV를 이용하게 되었다.

SMV를 이용한 논리식의 검증이 유망해진 까닭은 여러 가지가 있을 수 있겠지만, 대표적인 것으로는 논리식이 거짓일 때 반례(counterexample)를 사용자에게 보여준다는 것이며, 이는 사용자로 하여금 논리식을 적절히 고칠 수 있게 도와주는 기능을 한다. 아래의 그림 1은 SMV가 어떻게 작용하는 지를 그려놓은 그림이다. 그림에서와 같이 SMV는 사용자로부터 두가지를 입력받는다. 그것은 각각 □시스템 모델(System Description)□과 □검증 질의어(Assertion)□이다. 시스템 모델은 검사 대상이 되는 시스템을 SMV의 자체 입력 언어로 표현한 것이고, 검증 질의어는 사용자가 검사의 대상이 되는 시스템에 대한 질문인데, 주로 운전성과 안전성에 관련된 질문으로 구성된다. 모델 검사기(SMV)는 시스템의 동작을 표현하는 상태 공간을 검색하고 주어진 검증 질의어에 대해 참, 거짓으로 답변한다. 이때 거짓인 경우, 반례를 보여주게 된다. 본 글에서는 이러한 SMV의 장점인 반례를 찾는 알고리듬을 이용하여 불꽃 점화 공정의 안전 검색을 실시해 보겠다.

그림 1. SMV의 개요도[2]

Kripke 구조

Kripke 구조는 SMV의 반례찾기 알고리듬을 이해하기 위한 기본적인 데이타 구조이다. Kripke 구조 K를 다음과 같이 정의하고[3] 그림 2를 통해 예를 보여 설명하겠다.

K=(S, I, R, A, L)

1. S : 상태의 집합

2. I (⊆S) : 초기 상태의 집합

3. R (⊆SxS) : 상태간의 전이 관계를 나타내는 집합

4. A : 상태 구성 성분의 집합. A의 원소 a는 Da라는 도메인을 갖게 되며 이           는 참□거짓 값 혹은 정수 값을 갖는다.

5. L : L(s,a)의 함수 꼴로 나타내지며(s□S, a□A) Da에서 적절한 값을 반환           한다.

그림 2. (i) Kripke 구조         (ii) Kripke 구조에 기반한 computation tree

그림 2에서의 예에서 위의 1□5를 구체적인 값으로 나타내면 다음과 같다.

1. S={s0, s1, s2}

2. I={s0}

3. R={(s0, s1), (s0, s2), (s1, s0), (s2, s1)}

4. A={e, f, g}; De=Df=Dg={0, 1}

5. L(s0, e)=1, L(s0, f)=1, L(s1, f)=1, L(s1, g)=1, L(s2, e)=1, L(s2, g)=1

si□S, a□A인 다른 경우에 대해서는 L(si, a)=0

Computation Tree Logic

그림 2의 우측에 나타난 것이 computation tree이며, 이와 같이 각 상태들간의 관계를 시간에 따라, 경로에 따라 연결시키는 것을 computation tree logic(CTL)이라고 하며, CTL 식에는 일반적인 논리 연산자와 시간을 다루는 연산자로 나뉘며 여기에는 경로 한정사와 상태 한정사가 있는데, 경로 한정사는 전체 경로를 의미하는 A와 일부 경로를 의미하는 E가 있으며, 상태 한정사에는 전체 상태를 나타내는 G, 다음 시간의 상태를 의미하는 X, 미래의 상태를 나타내는 F, □□까지□를 나타내는 U 등이 있다[1]. 이들 경로 한정사와 상태 한정사는 하나씩 쌍을 이루어 하나의 연산자로 이용된다. 이중 EX, EU, EG 등을 의미를 설명하면 다음과 같다.

그림 3. CTL 연산자

EXf : 현재의 상태에서 다음 진행되는 상태들 중에서 f가 참이 되는 상                태가 적어도 하나 이상 있다.

E[fUg] : 현재의 상태로부터 g가 참이 되는 상태까지 f가 참이 되는 경                로가 적어도 하나 이상 있다.

EGf : 현재의 상태에서부터 시작되는 경로 중에서 그 경로의 모든 상태                가 f를 가지고 있는 경로가 존재한다.

그림 3에 위의 CTL식을 수형도로 나타내었다.

Witness Generation Algorithm

반례는 CTL식 중에서 경로 한정사가 A일 때 생성되어질 수 있다. □어떤□을 의미하는 E의 경우에 반례를 보이려면 모든 경로에 대해서 CTL식이 거짓을 보여야하는데 이것은 거의 불가능할 뿐만 아니라 큰 의미가 있지 않다. 따라서 이런 경우에는 참값을 갖게 되는 실례(witness)를 보여줌으로써 CTL식이 거짓인지 참인지를 보여주게 된다. 결국, 반례와 실례는 의미는 상대적인 의미를 갖지만, 검사자로 하여금 검사의 결과로 반례 혹은 실례를 보여줌으로써 올바른 검증을 하도록 도와주는 역할을 한다.

다음은 EXf, E[fUg], EGf 등의 실례(witness) 생성 알고리듬을 적용하기 위한 예제이며 그림 4의 형태로 표현하였다. 이것은 보일러 시스템의 불꽃 점화 부분을 나타낸 것이며, 이 그림의 s5를 현재의 상태라 가정할 때 불꽃의 생성을 f라 하면 아래 표 1과 같은 알고리듬에 의하여 EXf의 결과를 계산 과정에 따라 정리하면 표 2와 같다. 표 3과 표 4는 각각 E[fUg]와 EGf의 생성 알고리듬을 나타낸다.

표 1. EXf의 실례 생성을 위한 알고리듬[4]

function EX-witness(state s, formula f)

S'=f(v')□{□v|s(v)□R(v,v')}

s'□S'

push(s', witness)

push(s, witness)

return(witness)

그림 4. 보일러 불꽃 점화 공정

표 2. EXf의 witness 생성

{□v|s(v)□R(v,v')} => {s5, s6, s7}

f(v') => {s7}

S' => {s7} □ {s5, s6, s7} = {s7}

s' => s7

push(s7, witness) => s7

push(s5, witness) => s5, s7

return(witness) => s5, s7

표 3. E[fUg]의 실례 생성을 위한 알고리즘

function EU-witness(state s, formula f, formula g)

Y=s

Z=Y

frontier=Y

list-Z=s

while (frontier□□) do

X=frontier□g

if (X□□)

loop

t□X

push(t, witness)

if(t=s)return(witness)

Z=pop(list-Z)

pred-X={□v'|t(v')□R(v,v')}

X=Z□pred-X

end loop

front-f=frontier□f

Y=Z□{□v|front-f(v)□R(v,v')}

frontier=Y□□Z

Z=f□Y

push(Z, list-Z)

end while

return(□)

표 4. EGf의 실례 생성을 위한 알고리즘

function EG-witness(state s, formula f)

g=EGf

loop

h=g□EXs

list-2=EU-witness(s,g,h)

if(list-2)=□)

list-1=append(s, list-1)

s'□g(v')□{□v'|s(v)□R(v,v')}

s=s'

else

witness=append(list-2, list-1)

return(witness)

end loop

참고문헌

1. S.T. Probst, G.J. Powers, D.E. Long and I. Moon, "Verification of a logically controlled, solids transport system using symbolic model checking," Computers & Chemical Engineering, vol.21, no.4, pp417-431, 1997.

2. I. Moon, G.J. Powers, J.R. Burch and E.M. Clarke, "Automatic verification of sequential control systems using temporal logic," AIChE vol.38, no.1, pp67-75, 1992.

3. E.M. Clarke, E.A. Emerson and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specificatons," ACM transactions of Programming Languages and Systems, 8:244-263, 1986.

4. K.L. McMillan, "Symbolic Model Checking: An approach to the state explosion problem," Kluwer Academic Publishers, 1993.