보일러 운전절차의 안전성 검색을 위한 SMV 모델 개발

이승훈, 문 일

연세대학교 화학공학과

Developement of SMV Models for Boiler Operating Procedures

Seunghoon Lee and Il Moon

Department of Chemical Engineering, Yonsei University

서론

화학공정중 플랜트에 열을 공급하고 스팀을 만드는 등의 역할을 하는 것이 보일러이다. 이러한 보일러는 운전이 까다롭고 Safety Interlock을 많이 적용시키고 있다. 보일러의 오동작이나 긴급 상황 발생시 공정 열원의 불안정으로 말미암아 모든 공정에 이상이 발생할 수 있다. 그러므로 조업자의 운전에 대한 숙련정도가 안전에 중요한 요소로 작용한다. 공정안전검색방법으로 HAZOP, FTA 그리고 전문가 시스템등이 있다. 하지만 이들 방법들은 공정의 규모가 거대화되어감에 따라 더욱 많은 인력과 시간을 투자해 수행하여야 하며 공정의 개선에 따른 변화가 생길 경우에 처음부터 다시 수행하여야 한다. 이러한 어려움을 극복하기 위해 제안되고 있는 것이 컴퓨터를 이용한 안전성의 검증의 자동화이다. 모쥴화된 SMV를 이용하여 모델을 세워 놓고 이를 컴퓨터를 이용하여 자동적으로 검색하면 된다. 이 경우에 일어날 수 있는 위험한 상황을 검증 질의어라는 것을 이용해 검색하게 된다. 이러한 예로 보일러를 선택하였다. 보일러에서 일어날 수 있는 위험한 상황으로써 가열로 내부의 농도가 증가하여 위험 수위에 이를 경우 점화시 폭발의 위험이 있으므로 보일러가 일정 범위이내에서 운전되는가를 검색하였다.

SMV의 이용

SMV(Symbolic Model Verifier)는 CTL(Computational Tree Logic)이라는 논리와 BDD(Binary Decision Diagram)를 이용하여 주어진 논리의 참과 거짓을 판별하는 방법이다. 이전의 SMV에 비하여 최근의 SMV는 BDD를 사용하기 때문에 이진 트리(Binary Tree)의 모든 상태(State)를 검색하지 않고 이것을 축소시키거나 반복되는 구간(loop)를 찿아 간략화하여 검색하게 되었다. SMV는 모델을 정의하는 부분과 이것에 의하여 검증 질의어를 검색하는 부분으로 크게 나누어 생각할 수 있다. 화학공정을 정의하여 모델로서 입력하고 이에 의한 안전성을 검색하기 위하여 검증 질의어를 세우게 된다. 이렇게 만들어진 모델과 질문을 검색하여 안전에 관한 검증 질의어가 참인지 거짓인지를 파악하고 거짓이 나올 경우 이에 해당하는 반례를 보여준다. 이것을 이용하면 문제가 발생할 수 있는 부분을 파악할 수 있다. 이러한 결과를 보고 모델에서 수정해야할 부분을 찾아 내고 이를 다시  검색을 함으로써 화학공정의 안전성을 향상시킬 수 있다. 이것은 화학공정의 설계시 안전성 검증을 수행할 경우 효과적이며 기존의 공정을 개선할 경우에 안정성을 향상시키는 역할을 할 것이다. 또한 이러한 자동화된 검증법을 사용하는 가장 큰 장점은 모델로 작성된 모든 경우를 검색하여 주기 때문에 신뢰도를 향상 시킬 수 있는 장점이 있다. SMV언어로 표현된 밸브 On/Off의 예를 아래에서 보였다.

< 밸브1이 열리면 밸브2도 열린다. >

next(valve2) : case

(valve1 = 1) :  (valve2 = 1) ;

1           :  (valve2 = 0) ;

esac ;

SMV의 보일러 모델

SMV를 이용한 보일러 모델의 구현은 그림1과 같그림 1 보일러 Start-Up 순서  은 순서를 모델로 하였다. 그림3 공정도에 따라 작성한 SMV 프로그램은 여러개의 모쥴로 구성되어 있다. 이러한 모쥴간의 관계를 그림으로 표현하면 그림2와 같다. 그림2에서 보는 바와 같이 SMV는 모쥴화가 되어 있어 기본적인 형태의 모델을 선정하여 확장이 가능하고 가열로 모델에서 보일러 모델로의 확장, 보일러 모델에서 스팀 제너레이터로의 확장등 목적하는 바로의 접근이 용이하다. 공정이 바뀌더라도 기본적인 모쥴은 바뀌지않고 모쥴간을 연결시키는 방법만 바뀌게 된다. 그러므로 본 연구 에서는 보일러에서 버너가 1개인 경우를 모델로 설정하였다. 위와 같이 제안된 공정에 대하여 모쥴을 추가시켜가며 확장을 하였고 이에 따라 모델에 대한 정확성의 검색을 위한 검증 질의어와 안전을 검색하기 위한 검증 질의어가 입력되	어 있다.

그림2. SMV의 모쥴간의 구조

그림3. Boiler의 공정도

SMV의 검증질의어

검증질의어는 질문에 대하여 참, 거짓을 판별하고 이러한 결과를 이용하여 안전성을 해석할 수 있다. 본 연구에서 가열로 내부의 농도가 일정 농도 이하로 운전되는가라는 질문을 AG(box.conc<9)라는 것으로 주어 안전성을 검색하였다. 보일러의 조작순서에 따라 먼저 드럼을 채우고 팬을 가동시킨후 가열로에 오일을 공급하여 버너를 점화하는 순서에 따라 프로그램을 작성하였다. 대부분의 장치는 모쥴로 작성하여 버너의 수가 바뀌어도 간단한 과정으로 수정이 가능하고 임의의 장치가 공정에  미치는 영향을 살펴보기 위해서는 그 장치를 나타내는 변수를 nondeterministic variable로 하여 프로그램의 간단한 수정으로 그 장치가 공정에 미치는 영향을 추정해 볼 수 있다. 아래는 valve의 position에 관한 variable을 nondeterministic variable로 바꾸는 것을 보여 준다.

next(valve.position) := case

(step = 1)  : {0,1,2} ;

(step != 1) : valve.position ;

esac ;

이를테면 공정중의 팬의 구동이 정상적이지 않을 때는 가열로 내부의 농도가 한계 범위를 넘어가게 되는 것을 알 수 있다. 이러한 경우에 개선하여야 할 부분을 SMV프로그램으로 작성하여 보다 안전한 공정으로 가는 방법을 모색할 수 있고 새로운 환경규약등이 제안되는 경우 검증 질의어를 통하여 문제가 될  수 있는 부분의 유무를 확인할 수도 있다. 최근의 SMV는 이전의 SMV에 비하여 공정을 보다 세밀하게 표현하는 방법이 발달하여 있고 본 연구에서도 이러한 방법을 이용하였다. 다시 말하면 기존에는 밸브의 On/Off만을 표현하여 왔으나 이것을 밸브의 위치에 따라 여러 단계로 나뉘어 표현하고 이로부터 영향을 받는 변수들도 보다 구체적으로 표현하게 되었다. 이를테면 밸브의 위치에 따른 이전의 SMV의 표현방식은 아래와 같다.

next(valve) := case

(fan = 1)&(pump_run = 1) : 1 ;

1                       : 0 ;

esac ;

위와 같은 표현 방식에서 밸브의 위치를 완전 열림, 반 열림, 닫힘의 형태로 인식할 수 있도록 함으로서 보다 세밀한 표현을 할 수 있다. 이러한 방법의 발달로  실제의 공정에 보다 현실적으로 접근할 수 있다.

next(position) := case

(position != 0)&(fan = 1)&(pump_run = 1) : position + 1 ;

1                                      : 0 ;

esac ;

결과

앞에서 살펴본 바와 같이 SMV를 이용하여 보일러의 start-up과 운전중의 안전성을 검증하였다. 본 연구에서 모델로 선정한 보일러의 경우에 정상적인 조작의 경우 가열로 내부의 농도가 일정 수준이상으로 올라가지 않는다는 결과를 얻어 낼 수 있었고 임의의 장치가 오동작을 할 경우 공정에 미치는 영향을 SMV를 사용하여 확인할 수 있었다. 또한 각각을 소단위로 나누어 모쥴화 하였기 때문에 다소 복잡한 공정도 프로그램의 간단한 수정을 통하여 표현이 가능하다. 이렇듯 자동화된 방법으로 안전성 검증을 하는 것이 안전의 측면뿐만 아니라 인력과 비용의 측면에서도 많은 이점을 가진다.

참고 문헌

1. Scott 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, pp. 417-429, 1997.

2. Il Moon, G. J. Powers, J. R. Burch and E. M. Clarke, "Automatic Verification of Sequential Control Systems using Temperal Logic," AIChE vol.38, no.1, pp.67-75, 1992.

3. Il Moon, "Modeling PLCs for logic verification," IEEE Control Systems, vol.14, no.2, pp.53-59, April 1994.

4. 정상헌, 이광순, 문일, □공정의 안전 검증을 위한 PLC 모쥴 개발,□ 제어·자동화·시스템공학, vol.2, no.1, pp.53-59, 1996.