This study focuses on automatic verifying and validating methods for the safety and correctness of control logics of safety instrumented system (SIS) in chemical industrial processes. The models of discrete events, 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 using manual methods, 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.

A safety instrumented system (SIS) is one of the most important protective measurements in chemical plants and provides automatic actions to correct an abnormal process event or behavior that has not been controlled by basic control systems and manual interventions. SIS is composed of any combination of sensors, logic solvers, and final control elements for the purpose of taking the process to a safe state when predetermined conditions are violated. A SIS is commonly used on rare occasions including emergency shutdown system, safety shutdown system, and safety interlock system. A SIS, therefore, must be available to operate whenever needed. If SIS failure occurs, it is difficult to avoid from accidents such as explosion, process damage, environmental damage, loss of cost, and loss of human life. A SIS, thus, must be verified and validated thoroughly and systematically. Most of existing methods such as HAZOP (hazard and operability study), FTA (fault tree analysis), FMEA (Failure mode and effect analysis), etc. for identifying hazards, safety and reliability of SIS are commonly used in industrial field, but are usually very time consuming and only depend on manpower. Safety integrity level (SIL) is a standard for design of SIS and is used for specifying the safety integrity requirements of the safety instrumented functions to be allocated to the SIS. SIL offers information to define the probability of failure on demand, but it cannot verify the safety and reliability of SIS control logics. Simulators are often used to analyze the behavior of control systems and process variables based on a determined model. Although examining the output of simulation is sometimes helpful, in practice, this method is not proper to deal with discrete event and behavior because the SIS control logics commonly consist of signals, discrete variable or behaviors. The model checking verification method is an alternative approach that has achieved significant results recently. The main purpose of a model checker is verifying the model with regard to a requirement specification. Efficient algorithms are able to verify properties of extremely large systems. In these techniques, specifications are written as formulas in a proposition temporal logic and systems are represented by state-transition graph. The verification is accomplished by an efficient breadth first search procedure that views the transition system as a model for the logic, and determines if the specifications are satisfied by the model. There are several advantages to this approach. An important one is that the procedure is completely automatic. The model checker accepts a model description and specifications written as temporal logic formulas, and it determines if the formulas are true or not for that model.

In order to verify a process and SIS control logic, models for the process and the SIS control logic are developed respectively from the process descriptions and SIS control logic descriptions. Completeness and compactness of the model is the key issue in efficiently and correctly verifying the SIS control logics. The model description is a non-deterministic guarded command language with simple data (e.g. bounded integers, arrays, etc.). It serves as a modeling or design language to describe the process behavior (e.g. valve, pump, motor, etc) as networks of automata extended with time and SIS control process logics in chemical industrial processes. The idea is to model a process using automata and simulate it. Automata are a finite stat machine that is a graph containing a finite set of nodes or locations and a finite set of labeled edges. A system consists of a network of processes that are composed of locations. The system is modeled as a network of several such automata in parallel. The model is further extended with bounded discrete variables that are part of the state. A state of the system is defined by the locations of all automata and the values of the discrete variables. Every state may fire and edge separately or synchronize with another state, which leads to a new state. Transitions are used to change location and transitions between these locations define how the system behaves. To control when to fire a transition, it is possible to have a guard and synchronization. A guard is a condition on the variables saying when the transition is enabled. The synchronization mechanism is a hand-shaking synchronization: two processes take a transition at the same time, one will have a go! And the other a go?, go being the synchronization channel. The simulation of the constructed model is a validation which enables examination of possible dynamic executions of a system during early design stage and thus provides an inexpensive mean of fault detection prior to verification by model checker which covers the exhaustive dynamic behavior of the system. A graphical simulation which provides graphical visualization and recording of the possible dynamic and discrete behaviors of a description model of SIS control logic, i.e. sequence of symbolic stated of the control logic. It is also used to visualize traces generated by the model checker. The model checker is to check invariant and bounded-lively properties by exploring the state space of a system, i.e. reachability analysis in terms of symbolic states represented by constrains. Like the model, the requirement specification must be expressed in a formally well-defined and machine readable language. Several such logics exist in the scientific literature, and this study uses a simplified version of CTL (Computation Tree Logic). Like in CTL, the query language consists of path formula and state formula. State formula describe individual stated, whereas path formula quantify over paths or traces of the model. Path formula can be classified into reachability, safety and reliability. This study represents safety specification of SIS control system in chemical industrial processes. Different from normal control logic, SIS controls abnormal situation such as the emergency situation, control failure, abnormal signal and incorrect control logic program. The safe state of SIS control logic must be verified as part of the specification because all possible states are constructed in the part of model description. This study specifies the verification for the right location of controller, for the reliability of the SIS control logics and for the safe SIS control operation procedures and logics. Several case studies of chemical processes address the automatic and systematical verification of SIS control logic.

This study represents a novel approach to verify the safety of SIS control logic for chemical industrial processes using model checking. This method is applied to find the control logic error of SIS and unsafe procedures of SIS control operation. Based on the results, we can verify and validate the error-free SIS control logic and the right control location. An automatic verification method of SIS control logic is proposed to make sure that the control operations achieved by SIS are safe.

Keywords: safety instrumented system, control logic, safety verification, model checking, automatic