Modeling Programmable Logic Controllers for Logic Verification

Verification method has been developed for determining the safety and operability of programmable logic controller (PLC) based systems. The method automatically checks sequential logic embedded in PLCs and provides counterexamples if it finds errors. The method consists of a system model, assertions, and a model checker. The model is a Boolean-based representation of a PLC's behavior. Assertions are questions about the behavior of the system, expressed in temporal logic. The model checker generates a state space based on the above two inputs, searches the space efficiently, determines the consistency of the model and assertions, and supplies counterexamples. A modeling technique has been developed to verify relay ladder logic (RLL), a PLC programming language. The performance of the model checker is studied in a series of alarm designs.