Verification of a logically controlled, solids transport system using symbolic model checking

Scott T. Probst, Gary J. Powers, D. E. Long, I. Moon

Research output: Contribution to journalArticlepeer-review

22 Citations (Scopus)


Symbolic model checking has been used to formally verify safety and operability specifications on an industrial solids handling process. The fundamental principles behind symbolic model checking are presented along with techniques used to model process hardware, relay ladder logic control instructions, and human operating procedures for verification purposes. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.

Original languageEnglish
Pages (from-to)417-429
Number of pages13
JournalComputers and Chemical Engineering
Issue number4
Publication statusPublished - 1997

Bibliographical note

Funding Information:
Acknowledgements--This research has been supported by the National Science Foundation (grant DMC-6816889). We also thank Sergio Campos, a graduate student in Carnegie Mellon's School of Computer Science, for his help in interpreting SMV output.

All Science Journal Classification (ASJC) codes

  • Chemical Engineering(all)
  • Computer Science Applications


Dive into the research topics of 'Verification of a logically controlled, solids transport system using symbolic model checking'. Together they form a unique fingerprint.

Cite this