Range and Value-Set Analysis for Programmable Logic Controllers

This paper presents an analysis to infer range and value-set information for programs operating on programmable logic controllers. Given a program, the algorithm gathers all possible values of all variables for all possible program executions using abstract simulation. The set of these values constitutes an over-approximation of the program behavior and can thus be used to directly detect potential misbehavior. Crucially for practical applications, this approach works automatically without preprocessing or manual intervention. The approach is implemented in the Arcade.PLC framework and evaluated on a case study from industry.