Boolean and Modular Abstractions for Programmable Logic Controllers

This paper introduces a Boolean and a modular abstraction of programs for programmable logic controllers in order to make them amenable for formal verification. In the Boolean abstraction, complex control-flow conditions are replaced by fresh Boolean input variables to defer the evaluation of such conditions. The modular abstraction replaces function block calls by so-called function block summaries, which over-approximate their possible return values. Both abstractions can subsequently be refined in an automatic process to allow for checking of complex programs using expressive formulae. The approach has been implemented in the Arcade.PLC model checker, which is used to show the effectiveness in a case-study.