Event modeling and verification of chemical processes using symbolic model checking

Detection of faults related to issues of safety and quality can lead to a more dependable process. With current industrial practices, analysis of a modest sized process is difficult due to their large state space. Fortunately, improved fault detection for chemical processes can be obtained with the aid of symbolic model checking. In particular, SMV has been used to uncover faults in large, complex and sequential systems. In order to verify a chemical process, a finite state representation of the process is built. This dissertation presents a procedure for the synthesis of a non timed discrete model which captures the relevant continuous dynamics and sequential phenomena of the chemical process.; The procedure builds a discrete model of the chemical with the aid of the specifications which identify the relevant causal paths. The procedure searches backwards along these causal paths in constructing the transition relations for the state variables from the physical system, control systems, operating procedures, and operator behavior. The transition relations of the state variables represent the sequential phenomena of the chemical process along with its continuous dynamics and gains in the discrete model. The discrete values of the transition relations are based upon the division of the continuous value domain by landmarks and setpoints from the chemical process. This proposed procedure builds a discrete model for verifying the safety and operability of the chemical process. Before verification, the discrete model is validated by model checking properties observed during normal operation.; The synthesis procedure for a discrete model was applied to three industrial examples: a leak test procedure, a thermal oxidation process, and a coiled material transport process. The modeling of these industrial examples demonstrates the ability of the procedure in representing a chemical process. All three examples were verified with the aid of symbolic model checking. The verification results for these examples did not reveal any faults during normal operation, but several were discovered with the addition of failures and disturbances to the models. The model synthesis procedure and the method for validation aid in reaching the goal of verification for creating safe and reliable systems.