Model checking for automatic verification of control logics in chemical processes

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.