A methodology for synthesizing logic models of operating procedures for process verification

To ensure the safety and operability of a chemical process, fault detection has become an increasingly important aspect of process design. The analysis techniques typically employed by professional engineers include fault tree analysis, hazards and operability analysis (HAZOP), hazard surveys, hazard checklists, or any of a number of probabilistic analyses. In this thesis, the use of Symbolic Model Verification (SMV) as a process hazards analysis technique in demonstrated. Because SMV is a form of model checking, this method has the benefit of being able to verify the entire state space of a chemical system, including all of the combinations of behaviors present. Additionally, by utilizing a symbolic representation of a process model, SMV has the ability to analyze much larger systems than is currently possible by other methods.; Several difficulties are encountered when attempting to use SMV to verify a chemical system. The most important limitation to its use as a common verification tool is the time and resources necessary to create an accurate logic model representative of the process. At the present time, we are able to verify small industrial processes, but the amount of time necessary for model construction makes it infeasible to verify large systems. In this thesis, a method is developed that begins to address this problem.; A chemical system is composed of many parts, each of which must be accurately represented in the model. Operating procedures are represented in the models in a variety of different ways, depending on the type of procedure. In order to achieve an accurate representation of the system, human interaction with the process should be modeled to account for the types of behaviors that are unique to human operators. The modeling and verification of two industrial examples is used to demonstrate how models of operating procedures are created.; Through the analysis of operating procedure models created for SMV verification, several general rules for operating procedure modeling were derived and are described here. Based on these rules, a language for writing operating procedures, Verification - Operating Procedure Language (V-OPL), was developed. A translator was developed to allow for an operating procedure written in V-OPL to be automatically converted to an SMV logic model. Since it is much simpler to write an operating procedure in V-OPL than to create the logic model of the procedure for SMV verification, the time to create a model of a chemical process is reduced. The utilization of this modeling technique is demonstrated with industrial examples to evaluate its benefits and shortcomings.