Error-free scheduling for batch processes using symbolic model verifier

Jinkyung Kim, Jiyong Kim, Il Moon

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


This paper focuses on the development of a new approach for the synthesis of error-free operating schedules in batch processes. The synthesis of error-free operating procedures for batch processes becomes an important issue in the safe operation of industrial plant. It spends considerable amount of time and effort in scheduling and verifying operating procedures for correctness and completeness. In this study, we adopted SMV (Symbolic Model Verifier), an automatic error finding system, which is applied to various batch processes to test their safety and feasibility. The strength of this method is to minimize safety hazard and operability errors, and adjust process and recipe changes during the planning of operating procedure. The proposed approach identifies embedded errors and finds a minimum makespan and synthesizes an error-free operating sequence at the same time. Several examples are presented to illustrate the effectiveness of the proposed approaches.

Original languageEnglish
Pages (from-to)367-372
Number of pages6
JournalJournal of Loss Prevention in the Process Industries
Issue number4
Publication statusPublished - 2009 Jul

All Science Journal Classification (ASJC) codes

  • Control and Systems Engineering
  • Food Science
  • General Chemical Engineering
  • Safety, Risk, Reliability and Quality
  • Energy Engineering and Power Technology
  • Management Science and Operations Research
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Error-free scheduling for batch processes using symbolic model verifier'. Together they form a unique fingerprint.

Cite this