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

Jinkyung Kim, Il Moon

Research output: Contribution to journalArticle

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.

Original languageEnglish
Pages (from-to)1654-1661
Number of pages8
JournalKorean Journal of Chemical Engineering
Volume27
Issue number6
DOIs
Publication statusPublished - 2010 Oct 18

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)

Fingerprint Dive into the research topics of 'Automatic verification of operating schedules for batch processes using symbolic model checking: Latch model vs. real-time'. Together they form a unique fingerprint.

  • Cite this