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 journalArticle

16 Citations (Scopus)

Abstract

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
Volume30
Issue number1
DOIs
Publication statusPublished - 1997 Jan 1

Fingerprint

Control systems
Binary decision diagrams
VLSI circuits
Alarm systems
Moon
Model checking
Explosions
Data storage equipment
Testing
Processing

All Science Journal Classification (ASJC) codes

  • Chemistry(all)
  • Chemical Engineering(all)

Cite this

Moon, il ; Ko, Daeho ; Probst, Scott T. ; Powers, Gary J. / A symbolic model verifier for safe chemical process sequential control systems. In: Journal of Chemical Engineering of Japan. 1997 ; Vol. 30, No. 1. pp. 13-22.
@article{752fed8e43f24f88922dfb85109d5e44,
title = "A symbolic model verifier for safe chemical process sequential control systems",
abstract = "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.",
author = "il Moon and Daeho Ko and Probst, {Scott T.} and Powers, {Gary J.}",
year = "1997",
month = "1",
day = "1",
doi = "10.1252/jcej.30.13",
language = "English",
volume = "30",
pages = "13--22",
journal = "Journal of Chemical Engineering of Japan",
issn = "0021-9592",
publisher = "Society of Chemical Engineers, Japan",
number = "1",

}

A symbolic model verifier for safe chemical process sequential control systems. / Moon, il; Ko, Daeho; Probst, Scott T.; Powers, Gary J.

In: Journal of Chemical Engineering of Japan, Vol. 30, No. 1, 01.01.1997, p. 13-22.

Research output: Contribution to journalArticle

TY - JOUR

T1 - A symbolic model verifier for safe chemical process sequential control systems

AU - Moon, il

AU - Ko, Daeho

AU - Probst, Scott T.

AU - Powers, Gary J.

PY - 1997/1/1

Y1 - 1997/1/1

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

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

UR - http://www.scopus.com/inward/record.url?scp=0031070821&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0031070821&partnerID=8YFLogxK

U2 - 10.1252/jcej.30.13

DO - 10.1252/jcej.30.13

M3 - Article

AN - SCOPUS:0031070821

VL - 30

SP - 13

EP - 22

JO - Journal of Chemical Engineering of Japan

JF - Journal of Chemical Engineering of Japan

SN - 0021-9592

IS - 1

ER -