| Logic models, combined with model checking and Symbolic Model Verification (SMV), are useful for analyzing the safety and reliability of chemical processes. Traditional tools for analyzing and improving the safety of chemical processes such as checklists, HAZOPs, FTAs, and simulations are limited in their ability to investigate all the behaviors of the system being analyzed. However, verification considers the entire state space of a model, and is able to find problems, such as flaws in the process design or bugs in the control system, which may be missed by typical traditional safety testing. A logic model describes the system as a finite set of states and describes how transitions between those states are made (this can be called a nondeterministic finite automaton (NFA)). Specifications are written in Computation Tree Logic (CTL), a branching-time temporal logic. The model checking algorithm determines whether each specification is true or false and for each false specification gives a counterexample, a path through the system that demonstrates how the specification is violated. Logic models are different from typical chemical engineering models because they do not contain continuous variables (and by extension differential equations). Logic models may only contain variables with types of boolean, integer range, or enumerated set. The difficulties that must be overcome in order to create a logic model of a chemical process are: (1) discretizing continuous physical variables, (2) preserving the dynamic (rate) information, and (3) capturing all known behaviors. Previously, creating logic models of chemical processes has been a difficult and time consuming process. This thesis presents a method for creating modular logic models of chemical systems which addresses the three difficulties above and is faster than previous modeling techniques. A framework for storing and cataloging logic models of common chemical engineering units is defined and several basic unit modules are included in the library. Also, a procedure for synthesizing complex logic models using pre-exiting modules from the library is demonstrated. The effectiveness of the model synthesis procedure is shown using an industrial example. |
