Symbolic Execution of Programmable Logic Controller Code

Programmable logic controllers (PLCs) are specialized computers for automating a wide range of cyber-physical systems. Since these systems are often safety-critical, software running on PLCs need to be free of programming errors. However, automated tools for testing PLC software are lacking despite the pervasive use of PLCs in industry. We propose a symbolic execution based method, named SYMPLC, for automatically testing PLC software written in programming languages specified in the IEC 61131-3 standard. SYMPLC takes the PLC source code as input and translates it into C before applying symbolic execution, to systematically generate test inputs that cover both paths in each periodic task and interleavings of these tasks. Toward this end, we propose a number of PLC-specific reduction techniques for identifying and eliminating redundant interleavings. We have evaluated SYMPLC on a large set of benchmark programs with both single and multiple tasks. Our experiments show that SYMPLC can handle these programs efficiently, and for multi-task PLC programs, our new reduction techniques outperform the slate-of-the-art partial order reduction technique by more than two orders of magnitude.