A symbolic model verifier for safe chemical process sequential control systems

We have developed a symbolic verification method for determining the safety and operability of chemical process sequential control systems. The number of test cases required to verify a system grows exponentially as the number of components of the system increases. This state explosion 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 originally developed by McMillan to test VLSI circuits. The method uses Boolean formulas to represent sets and relations in order to avoid building an explicit state transition graph which occupies most of the computer memory consumed for the computation. Ordered Binary Decision Diagrams are employed to manipulate the formulas efficiently in the model checking process. As a result, the SMV can verify large alarm systems including 10¹²¹ reachable states. The input language of SMV also makes the modeling of chemical processing systems as easy and less error prone processes. The method is demonstrated and the performance of the verifier is studied in a series of multiple alarm designs.