Programmable logic controllers (PLC's) are used extensively for complex embedded control applications such as factory control in manufacturing industries and for entertainment equipment in amusement parks. Relay Ladder Logic (RLL) is the most widely used PLC programming language; approximately 50% of the manufacturing capacity in the United States is programmed in RLL. RLL is a legacy programming language, with a very low-level and complex semantics. From the point of view of building tools to detect errors, the design of RLL is at least unhelpful, and may in fact represent something like a worst case. However, there is a manifest need for such tools. The validation of RLL programs is extremely expensive, often measured in millions of dollars (for factory down-time) or human safety (for rides). RLL programs are represented as stylized circuit diagrams, with some number of one-bit inputs and outputs. Inputs are attached to sensors, while outputs are attached to actuators. RLL programs are evaluated by an interpreter that simulates the circuit, reading new inputs and updating outputs. RLL programs may have state (i.e., latches). One evaluation of the circuit is called a scan; the interpreter executes the circuit, scan after scan, indefinitely. The complexity of RLL arises mainly from the interaction of the interpreter with the language, which has special instructions that can alter the interpreter's behavior by e.g., skipping portions of the circuit. It is these imperative control features that render standard techniques for analyzing circuits unsuitable for analyzing RLL.
Our analysis tools are constraint-based, meaning that the properties of interest are expressed as constraints generated from the program text. Solving these constraints yields the desired information. The analysis has two phases: