Automated verification of safety and operability specifications of chemical processes

The safety and operability of chemical processes is very important in the chemical process industries. However, chemical processes are combinations of interacting discrete and continuous systems, or hybrid systems, for which the verification of safety and operability specifications is a difficult task.; This dissertation describes algorithms that use linearization techniques and a conservative, discrete approximation of the continuous systems to greatly reduce the computational effort required to verify the safety and operability specifications of chemical processes. In particular, the Transition Relation Updating Procedure (TRUP) iteratively generates the discrete model in “closed-loop” mode during the “reachable states computation”, thus greatly reducing the number of states to be analyzed. The Linear Forward Mapping Procedure (LFMAP), which was also developed in this work, is used within the TRUP to calculate connections between the discrete states. The LFMAP greatly reduces, compared to the originally proposed approaches, computational effort by using linear techniques. The algorithms were implemented in a prototype software package named VIS_SGA.; VIS_SGA uses the algorithms developed together with Symbolic Model Checking and was applied to four benchmark examples from the literature. VIS_SGA was used to verify safety and operability specifications stated in Computation Tree Logic for a two-tank example, a nuclear reactor example, a batch evaporator example, and a batch reactor example. The results showed that VIS_SGA and therefore the algorithms that were developed can be used to: verify higher-dimensional problems (two-tank example); perform a parametric analysis (nuclear reactor example); detect faulty programmable logic controller code and determine appropriate sensor settings (batch evaporator example); and determine ranges of starting conditions for which operability specifications are satisfied (batch reactor example). Furthermore, the results showed that VIS_SGA could be used to accurately simulate all of the benchmark examples.