A SYMBOLIC MODEL VERIFIER FOR SAFE CHEMICAL PROCESS SEQUENTIAL CONTROL-SYSTEMS

We have developed a symbolic verification method for determining the s afety and operability of chemical process sequential control systems, The number of test cases required to verify a system grows exponential ly as the number of components of the system increases, This state exp losion problem limits our previous automatic verification method (Moon et al., 1992, Moon, 1994) to testing small systems, To mitigate this problem, we have adopted the Symbolic Model Verifier (SMV) which was o riginally developed by McMillan to test VLSI circuits. The method uses Boolean formulas to represent sets and relations in order to avoid bu ilding an explicit state transition graph which occupies most of the c omputer memory consumed for the computation. Ordered Binary Decision D iagrams are employed to manipulate the formulas efficiently in the mod el checking process. As a result, the SMV can verify large alarm syste ms including 10(121) reachable states, The input language of SMV also makes the modeling of chemical processing systems as easy and less err or prone processes. The method is demonstrated and the performance of the verifier is studied in a series of multiple alarm designs.