갠트차트로 표현되는 회분공정의 운전절차를 검색하여 안전성과 실현가능성을 확인하는 방법을 개발하였다. 본 연구에서는 처음으로 SMV(Symbolic Model Verifier)를 이용하여 갠트차르를 표현하는 방법을 두 가지로 제시하고 이를 비교, 분석하였다. 시간에 대한 표현 방법에 따라 실시간 변수(real time variable)를 이용하는 방법과 래치 변수(latch variable)를 이용하는 방법의 두 가지로 알고리듬을 제시하고 이 두가지 SMV 알고리듬의 효율성을 비교한 결과, 실시간 모델(real time model)이 검색시간과 검색해야 할 가지의 수에서 상대적으로 우수한 것으로 나타났다. 또한 SMV의 질의어를 통해 갠트차트로는 표현하기 어려운 공정 또는 생산품의 특성에 관련한 오류를 찾아 낼 수 있었다. 이를 통해 보통의 갠트차트로는 찾기 어려운 회분식 생산공정의 오류들을 자동으로 검색 할 수 있는 방법을 제시하였다.

A new algorithm is proposed to detect errors in process schedules using SMV(symbolic model verifier). Two models, real time model and latch model, are developed to capture information on Gantt charts. The real time model is proved to be more efficient than the latch model. In addition, they can find errors related to the characteristics of the process and the product, which are difficult to be detected only by Gantt chart. It proves that the proposed algorithm can automate the procedure of detecting errors in batch process schedules.

Symbolic Model Verifier Batch Process Schedule Real Time Model Gantt Chart

Ko D, Moon I, Comput. Chem. Eng., 21(S), 1067 (1997)
Moon S, Bok J, Park S, HWAHAK KONGHAK, 35(5), 599 (1997)
Ko D, Moon I, HWAHAK KONGHAK, 35(3), 338 (1997)
Biegler LT, Grossmann IE, Westerberg AW, "Systematic Methods of Chemical Process Design," Prentice Hall, 187 (1997)
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang J, "Symbolic Model Checking: 10(20) States and Beyond," In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (1990)
Moon I, Powers GJ, Burch JR, Clarke EM, AIChE J., 38(1), 66 (1992)
Moon I, IEEE Control. Systems, 14(2), 53 (1994) 
Jeong S, Lee K, Moon I, ICASE, 2(1), 53 (1996)
Probst ST, Powers GJ, Long DE, Moon I, Comput. Chem. Eng., 21(4), 417 (1997) 
Probst ST, Powers GJ, "Automatic Verification of Chemical Process in the Presence of Failure Modes," AIChE Annual Meeting, San Francisco, CA (1994)