Symbolic execution of programmable logic controller code
- 21 August 2017
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- p. 326-336
- https://doi.org/10.1145/3106237.3106245
Abstract
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 state-of-the-art partial order reduction technique by more than two orders of magnitude.Keywords
This publication has 43 references indexed in Scilit:
- Speeding Up the Safety Verification of Programmable Logic Controller CodeLecture Notes in Computer Science, 2013
- Predicate Abstraction for Programmable Logic ControllersLecture Notes in Computer Science, 2013
- Simulation framework for the verification of PLC programs in automobile industriesInternational Journal of Production Research, 2011
- Cloud9ACM SIGOPS Operating Systems Review, 2010
- Peephole Partial Order ReductionPublished by Springer Science and Business Media LLC ,2008
- Interrupt Verification via Thread VerificationElectronic Notes in Theoretical Computer Science, 2007
- Symbolic Execution with Abstract Subsumption CheckingLecture Notes in Computer Science, 2006
- Model Checking Real Time Java Using Java PathFinderLecture Notes in Computer Science, 2005
- Model-Checking Middleware-Based Event-Driven Real-Time Embedded SoftwareLecture Notes in Computer Science, 2003
- Detecting races in relay ladder logic programsPublished by Springer Science and Business Media LLC ,1998