Dynamically detecting invariants for automatic testing PLC programs

Since programmable logic controllers (PLCs) control safety-critical infrastructures, examining the PLC software satisfies the high-reliability specifications necessary to ensure the safeness of PLCs. However, prior works have limitations in finding defects in the PLC source code. Static verification techniques suffer from notable false positives without capturing runtime behavior. The symbolic execution and conformance testing technique captures the relations of inputs and outputs. It is not sufficient to consider only the data constraints as the PLC operates in real-time. In this paper, we propose a novel approach in the detection of the runtime behavior of PLC programs with incorporated time constraints. This testing approach automatically finds implementation errors in PLC programs by mining invariants from runtime traces. As the existing tools mine only data or time invariants which are inadequate to test PLC programs, our approach focuses on the interplay of data and time invariants. Dynamically detected data-time invariants are then checked with the safety specifications. We evaluate the usefulness of our approach in a real-life case. The experimental results show that the proposed approach can find errors in PLC programs effectively.