A symbolic model verifier for safe chemical process sequential control systems

Il Moon, Daeho Ko, Scott T. Probst, Gary J. Powers

Research output: Contribution to journalArticlepeer-review

17 Citations (Scopus)


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 10121 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.

Original languageEnglish
Pages (from-to)13-22
Number of pages10
JournalJournal of Chemical Engineering of Japan
Issue number1
Publication statusPublished - 1997 Feb

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)


Dive into the research topics of 'A symbolic model verifier for safe chemical process sequential control systems'. Together they form a unique fingerprint.

Cite this