| Chemical process hazards which arise as a result of faulty control logic or human operating procedures may be difficult to detect. The complex sequential and combinational functionality of these systems results in a very large number of possible behaviors, some of which may contain faults. A formal verification method called symbolic model checking has been used to verify some example chemical processes. The strength of symbolic model checking is that it can search exhaustively for faults contained within a user-defined model. Desired properties of the system are expressed in temporal logic, and are algorithmically verified with respect to the model. When safety or operability properties are violated, counterexamples may be generated which demonstrate how a violation may occur. Modeling techniques for representing time, control logic, process equipment, human operating procedures, and failure modes have been developed. Example systems verified include a solids transport system controlled by a programmable logic controller (PLC), a maintenance procedure for checking valve tightness in a furnace system, a batch reactor system controlled by a PLC involving strong human interaction, and a furnace system standard defining required hardwired logic, software interlocks, and process equipment. Compositional verification techniques were used to check properties of the furnace standard. |
