Model checking for automatic verification of control logics in chemical processes

Jinkyung Kim, Il Moon

Research output: Contribution to journalArticle

6 Citations (Scopus)

Abstract

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
Volume50
Issue number2
DOIs
Publication statusPublished - 2011 Jan 19

Fingerprint

Model checking
Industrial chemicals
Discrete event simulation
Process control
Industry

All Science Journal Classification (ASJC) codes

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

Cite this

@article{45ba5308a38a4f45a3b2d736ef9170a6,
title = "Model checking for automatic verification of control logics in chemical processes",
abstract = "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.",
author = "Jinkyung Kim and Il Moon",
year = "2011",
month = "1",
day = "19",
doi = "10.1021/ie100007w",
language = "English",
volume = "50",
pages = "905--915",
journal = "Industrial & Engineering Chemistry Product Research and Development",
issn = "0888-5885",
publisher = "American Chemical Society",
number = "2",

}

Model checking for automatic verification of control logics in chemical processes. / Kim, Jinkyung; Moon, Il.

In: Industrial and Engineering Chemistry Research, Vol. 50, No. 2, 19.01.2011, p. 905-915.

Research output: Contribution to journalArticle

TY - JOUR

T1 - Model checking for automatic verification of control logics in chemical processes

AU - Kim, Jinkyung

AU - Moon, Il

PY - 2011/1/19

Y1 - 2011/1/19

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=78651399472&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=78651399472&partnerID=8YFLogxK

U2 - 10.1021/ie100007w

DO - 10.1021/ie100007w

M3 - Article

AN - SCOPUS:78651399472

VL - 50

SP - 905

EP - 915

JO - Industrial & Engineering Chemistry Product Research and Development

JF - Industrial & Engineering Chemistry Product Research and Development

SN - 0888-5885

IS - 2

ER -