SMV를 이용한 회분공정 생산일정의 안전성 평가

이한용, 김진경, 윤형준, 문일+

연세대학교 화학공학과

Verification of the Safety of the Batch Process Schedules

using a Symbolic Model Verifer

Hanyong Lee, Jinkyoung Kim, Hyungjoon Yoon and Il Moon+

Department of Chemical Engineering, Yonsei University

연구배경

회분식 공정은 특성상 복잡하며 생산계획과 실제 생산상의 불일치로 인한 외란이 발생하기 쉬운 단점이 있다. 생산계획 또한 이러한 외란을 고려하여 정확하게 만들어져야 하므로 복잡한 양상을 띠게 되었다[1,2]. 따라서 점차로 복잡해지는 생산계획은 이전보다 다양한 오류에 대한 가능성을 내포하고 있다[3]. 제품들의 특성상 고려되어야 하는 다양한 생산방법에 따른 오류들은 단순히 갠트차트만을 통해서는 찾기가 어려운 문제이다[4].

그럼에도 불구하고 주어진 회분공정의 생산일정에 대한 안전성에 대한 연구는 전무하다. 따라서 본 연구에서는 오류들의 다양한 형태를 SMV(Symbolic Model Verifier)를 통해 자동적인 생산일정상의 오류 검색 알고리듬을 제시하고 주어진 생산일정의 안전성(safety) 및 실현 가능성(feasibility)에 대한 평가를 수행하였다.

연구수행절차

본 연구에서는 SMV를 통하여 다양한 형태의 생산일정 검색을 수행할 수 있는 알고리듬을 개발하였다. SMV에서 생산일정을 표현하는 방법에 대한 연구를 수행하고 이에따라 다양한 형태의 공정 및 생산품의 특성을 표현하였다.

이러한 알고리듬을 이용하여 주어진 공정을 중심으로 SMV상에서 표현을 하고 적절한 질의를 CTL(Computational Tree Logic)로 나타냄으로써 오류를 효과적으로 찾아낼 수 있는가를 검토하였다[그림 1]. 주어진 공정은 4단으로 구성된 공정으로서 생산물 A만이 Zero-Wait Policy를 따르고 Mixer를 제외한 나머지 공정이 스팀을 공유함으로써 제한요소를 가지는 것으로 구성하였다.

주요 연구내용

- 회분공정의 생산일정은 생산품들의 순서에 관련한 함수로서 표현되며 이러한 요소를 SMV상에서 구현하기위한 모델의 알고리듬을 개발하였다. 알고리듬은 공정의 상태변수들이 생산순서의 함수에 종속적으로 모두 동기화될 수 있도록 고려하여 하나의 BDD(Binary Decision Diagram)에 공정과 관련한 모든 상태함수를 표현하였다.

- 주어진 공정을 SMV상에서 표현하고 공정의 특성 및 생산품의 특성으로 생기는 제한요소에 관하여 CTL을 통해 검증하였다.

그림 . 제한요소를 가지는 회분공정

SMV를 이용한 생산일정의 구현

실제로 시간을 SMV상에서 구현한다는 것은 어려운 일이다. 그러나 시간을 일정한 구간으로 나누고 구간별로 상태의 함수를 만듬으로써 생산일정을 표현할 수 있었다.

또한 각 공정은 순서의 함수를 참조하면서 서로 동기화되어야만 공정들의 순서적인 배열을 표현할 수 있다. 따라서 모듈화된 각 공정의 함수 안에 공정상태에따른 순서적인 시간의 함수를 따로 내장하여 전체 조업시간의 모듈에 연결시킴으로써 정확한 조업순서의 표현과 각 공정들 사이의 동기화를 구현하였다.

우선 각 공정이 한가지 생산물에대한 조업상태를 나타낼 수 있도록 Exclusive OR의 개념을 SMV에 도입하여 나타내었다[그림 2]. 이러한 개념과 정하여지지 않은 변수(undetermined variable)를 이용, 초기에 첫 번째 단에서 공급하는 생산물을 한가지만 선택할 수 있도록 하여 자동적으로 어떠한 생산물을 먼저 생산하든간에 오류가 일어날 수 있는 모든 가능성을 검색할 수 있도록 하였다.

그리고 각 장치별로 순차적인 동기화를 이룸으로써 전체적인 공정이 하나의 시간적인 관계에 놓일 수 있도록 구성하였다[그림 3].

생산일정상의 오류 검색

위와 같이 구성된 전체적인 공정의 알고리듬을 바탕으로 CTL (Computational Tree Logic)을 통해 제한요소들을 위반하는 경우는 없는지를 검색하였다. 제작된 SMV프로그램을 바탕으로 다음과 같은 제한요소에 관한 검증 질의어를 작성하였다.

검증 질의어 1.

동시에 Reactor02에서는 A를 조업중이고 Reactor01은 B가 조업중이며 Separator는 C가 조업중일 수는 없다

-> AG (( !( Reactor02 = A_on & Reactor01 = B_on & Seperator = C_on)))

검증 질의어 2.

Mixer에서 A의 조업이 끝난 경우 Reactor01이 조업중인 경우는 없다

-> AG (( !( Mixer = A_off & ( Reactor01 = B_on | Reactor01 = C_on))))

검증 질의어 3.

Reactor01에서 A의 조업이 끝난 경우 Seperator가 조업중인 경우는 없다.

-> AG (( !( Reactor01 = A_off & Seperator = C_on)))

검증 질의어 4.

Seperator에서 A의 조업이 끝난 경우 Reactor02가 조업중인 경우는 없다.

-> AG (( !( Seperator = A_off & ( Reactor02 = B_on | Reactor02 = C_on))))

검증질의어 1은 스팀을 공유하여 쓰는 세단계 장치의 특성에 관련한 오류를 검색하고자 하는 것이고, 나머지 세개의 검증질의어는 생산품 A의 특성과 관련하여 ZW Policy에 위배되는 오류를 검색하고자 하는 것이다.

검색결과 모두 오류가 일어날 수 있음이 판명되었다. 결과의 예시는 검증질의어 1과 관련한 것을 나타낸 것이다[그림 4]. 또한 각 검증질의어를 통해 검색한 시간 및 BDD의 가지수를 나타내었다[표 1].

결론

본 연구를 통하여 점차 복잡해지고 있는 회분공정의 생산일정을 자동적으로 검색할 수 있는 SMV알고리듬을 개발하고 이를 통해 오류의 가능성을 미리 검색할 수 있었다. 일반적으로 회분공정의 생산일정 검색에 사용되는 갠트차트를 SMV상에서 구현할 수 있었으며 갠트차트로는 표현하기 어려운 공정의 여러 가지 변수 및 제한요소들도 검증이 가능하였다.

참고문헌

1. Ko, D. and I. Moon, "Dynamic scheduling Algorithm in Case if Unit Failure for Batch Process Management," Comp. Chem. Eng., 21, 1067(1997).

2. Lee, H., Jung, J. H., Moon, I. and Lee, I., HWAHAK KONGHAK, 35, 599(1997)

3. Biegler, L.T., Grossmann, I.E and Westerberg, A.W., "SYSTEMATIC METHODS OF CHEMICAL PROCESS DESIGN," Prentice Hall, 187(1997).

4. Moon, I,. "Automatic verification of discrete chemical process control system," doctorial thesis, Carnegie Mellon University, (1992).

그림 . Exclusive OR 시작 모듈

그림 . Mixer 모듈

그림 . 검증질의어 1의 검색결과

검증질의어	1	2	3	4
user time	0.15 s	0.12 s	0.13 s	0.17 s
system time	0.07 s	0.07 s	0.07 s	0.05 s
BDD nodes allocated	4385	2694	3505	4698
Bytes allocated	917504	917504	917504	917504
BDD nodes representing transition relation	246	246	246	246

표 1. 검증질의어에 따른 자원 사용