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.
Bibliographical noteFunding 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