A PLC is a special purpose for industrial computer used to automate industrial processes. It can be connected to several inputs and outputs depending on the configuration of its internal state and the inputs. The PLC execution is following a cycle. The all inputs state is copied into memory. The internal program runs and creates in memory a temporary all outputs table. The table is written to the outputs and a new cycle starts when this program completes. It will repeat as long as the PLC is running.
A PLC can be programmed using the five languages which are: Instruction List, Structured Text, Function Block Diagram, Sequential Function and Ladder Diagram. The languages semantics is not strictly defined, certain definitions are missing or contain ambiguities.
Ladder Diagram is the most used PLCs programming language. It is a graphical language where the basic elements are based on an analogy to physical relay diagrams. The properties to be verified over an LD program could be generic and apply to every model or specific to one model. Model related properties must be formulated by the programmer, while generic properties only rely on the metamodel concepts and can be automatically generated from the model.
One of important properties of Logic Ladder to be verified on its program is the absence of race conditions. A race condition is an undesirable situation that occurs when a system or device attempts to perform two or more operations at the same time but because of the nature of the system or device, the operations must be done in the proper sequence in order to be done correctly. A race condition occurs in the Ladder Diagram program when under fixed inputs and function block states, one or more outputs keep changing their values. The variables of Ladder Diagram will not stabilize thus it is an example of race condition. This kind of problem is sometimes difficult to detect using traditional techniques.