Articles & Issues
- Language
- English
- Conflict of Interest
- In relation to this article, we declare that there is no conflict of interest.
- Publication history
-
Received January 3, 2010
Accepted February 17, 2010
-
This is an Open-Access article distributed under the terms of the Creative Commons Attribution Non-Commercial License (http://creativecommons.org/licenses/bync/3.0) which permits
unrestricted non-commercial use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright © KIChE. All rights reserved.
All issues
Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time
School of Chemical & Biomolecular Engineering, Georgia Institute of Technology, 311 Ferst Drive, NW, Atlanta, Georgia 30332, U.S.A., USA 1Department of Chemical Engineering, Yonsei University, 134 Shinchon-dong Seodaemun-gu, Seoul 120-749, Korea
Korean Journal of Chemical Engineering, November 2010, 27(6), 1654-1661(8), 10.1007/s11814-010-0272-x
Download PDF
Abstract
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.
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)
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)
