Computers & Chemical Engineering, Vol.21, No.4, 417-429, 1997
Verification of a Logically Controlled, Solids Transport-System Using Symbolic Model Checking
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.