Modeling and verification of control logics in safety instrumented system for chemical industrial processes

This study focuses on automatic verification and validation methods for the safety and correctness of control logics of the safety instrumented system (SIS) in chemical process industry. The models of discrete events, system behaviors and control programs for chemical processes and SIS are developed using automata theory. Symbolic model checking method, an automatic error finding approach, is used to verify its safety and reliability. The strength of this method is to synthesize a feasible sequence through a counter-example and to verify its correctness using computation tree logic (CTL) simultaneously. This method can be applied to determine the error-free location of SIS, to find the logical errors automatically which is difficult to find manually, and to verify the safety and feasibility of SIS. This paper addresses the model development of the SIS control logics of chemical industrial processes and presents how model checking approach can be used efficiently in the verification of SIS control logics through several case studies.