Model checking for automatic verification of control logics in chemical processes

Jinkyung Kim, Il Moon

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)


This study focused on the automatic verification and validation of the safety and correctness of chemical process control logics. Discrete events, system behaviors, and control logic of chemical processes were formally modeled as automata. The symbolic model checking method was used to verify its safety and reliability. The strength of this method is synthesizing a feasible sequence through a counter-example and simultaneously verifying its correctness using computation tree logic (CTL). The model checking method was applied to determine the error-free design of the control operating sequence and automatically find the logical errors. An automatic technique is proposed to provide and modify the P&ID design of control logics for the chemical process industry. This Article addresses the model development of the control logics for industrial chemical processes and presents several case studies to show how a model checking approach can be used for the efficient verification of control logics.

Original languageEnglish
Pages (from-to)905-915
Number of pages11
JournalIndustrial and Engineering Chemistry Research
Issue number2
Publication statusPublished - 2011 Jan 19

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)
  • Industrial and Manufacturing Engineering


Dive into the research topics of 'Model checking for automatic verification of control logics in chemical processes'. Together they form a unique fingerprint.

Cite this