Symbolic model verifier for formal testing of discrete process control systems

Abstract: "We have developed a symbolic verification method for testing discrete chemical process control systems including process equipment and control system software and hardware. The method automatically determines if the system behaves as specified by safety and operability requirements. The method consists of: 1) a system model describing the process and its software, 2) assertions expressing user-supplied questions about the system behavior and 3) a model checker testing if the system model satisfies the assertions and supplying a counterexample if an error exists. The assertions are expressed using temporal logic operators for reasoning about occurrence of events in time. This verification method symbolically inspects the elements of the model. Compared with our previous explicit state enumeration method (Moon, 1991), this symbolic method can handle larger systems and be more complete in its system description. The method has been tested on an alarm system to uncover discrete event sequencing errors."