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

作者：Kim Jinkyung; Moon Il^*

来源：Korean Journal of Chemical Engineering, 2010, 27(6): 1654-1661.

DOI：10.1007/s11814-010-0272-x

• Operating Schedule
• Real-time Model
• Latch Model
• SMV
• Batch Process

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.

• 出版日期2010-11