Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time

Jinkyung Kim; Il Moon

Korean Journal of Chemical Engineering, Vol.27, No.6, 1654-1661, November, 2010

DOI10.1007/s11814-010-0272-x Export Citation

Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time

Jinkyung Kim, and Il Moon^{1, †}

School of Chemical & Biomolecular Engineering, Georgia Institute of Technology, 311 Ferst Drive, NW, Atlanta, Georgia 30332, U.S.A., USA
¹Department of Chemical Engineering, Yonsei University, 134 Shinchon-dong Seodaemun-gu, Seoul 120-749, Korea

E-mail:

This study proposes two models for reading Gantt charts and finding embedded errors in the operating schedules of batch processes. Two automatic techniques for finding errors, a real-time model and a latch model, are developed using the symbolic model verifier (SMV) and are compared to verify that the schedules are error free and to represent the scheduling information and policies. These models are designed to automatically detect embedded errors relating to unavailability, superimpositions, and violation of intermediate storage policies in batch processes with various intermediate storage policies.

Keywords:Operating Schedule;Real-time Model;Latch Model;SMV;Batch Process

[References]

Kim J, Lee H, Moon I, The 8th APCChE Congress, Seoul, Korea (1999)
Lee H, Kim J, Moon I, AIChE Annual Meeting, Dallas, Texas (1999)
Reeve A, Process Engineering, 73, 33 (1992)
Kim J, Moon I, Comput. Chem. Eng., 24(2-7), 385 (2000)
Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang J, In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (1990)
Clarke EM, Emerson EA, Sistla AP, ACM Trans. on Programming Lang. Sys., 8, 244 (1986)
Moon I, Powers GJ, Burch JR, Clarke EM, AIChE J., 38, 66 (1992)
Moon I, Ko D, Probst ST, Powers G, J. Chem. Eng. Jpn., 30(1), 13 (1997)
Moon I, IEEE Control Systems, 14, 53 (1994)
Probst ST, Powers GJ, Long DE, Moon I, Comput. Chem. Eng., 21(4), 417 (1997)
Probst ST, Powers GJ, AIChE Annual Meeting, San Francisco, CA (1994)
Biegler LT, Grossmann IE, Westerberg AW, Systematic Methods of Chemical Process Design, Prentice Hall, Englewoodcliffs, NJ, 187 (1997)
Ko D, Moon I, Comput. Chem. Eng., 21(S), 1067 (1997)

[Related Articles]

[1] Kim J, Lee H, Moon I, The 8th APCChE Congress, Seoul, Korea (1999)

[2] Lee H, Kim J, Moon I, AIChE Annual Meeting, Dallas, Texas (1999)

[3] Reeve A, Process Engineering, 73, 33 (1992)

[4] Kim J, Moon I, Comput. Chem. Eng., 24(2-7), 385 (2000)

[5] Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang J, In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (1990)

[6] Clarke EM, Emerson EA, Sistla AP, ACM Trans. on Programming Lang. Sys., 8, 244 (1986)

[7] Moon I, Powers GJ, Burch JR, Clarke EM, AIChE J., 38, 66 (1992)

[8] Moon I, Ko D, Probst ST, Powers G, J. Chem. Eng. Jpn., 30(1), 13 (1997)

[9] Moon I, IEEE Control Systems, 14, 53 (1994)

[10] Probst ST, Powers GJ, Long DE, Moon I, Comput. Chem. Eng., 21(4), 417 (1997)

[11] Probst ST, Powers GJ, AIChE Annual Meeting, San Francisco, CA (1994)

[12] Biegler LT, Grossmann IE, Westerberg AW, Systematic Methods of Chemical Process Design, Prentice Hall, Englewoodcliffs, NJ, 187 (1997)

[13] Ko D, Moon I, Comput. Chem. Eng., 21(S), 1067 (1997)