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