Direct Model Checking of PLC Programs in IL

While there are several approaches applying model checking to PLC programs, it is still not used in industry. This is due to the limited applicability of the existing approaches, which all translate PLC programs into the input languages of existing model checkers and thus suffer from certain problems. This paper presents a new approach that applies model checking directly to PLC programs written in IL without using translations. This has some advantages: domain-specific information is available during verification, users can make propositions about all features of the PLC, and counterexamples are given in the same language as the program, thus, simplifying the process of locating errors. In the described approach, a tailored simulator builds the state space for verification. Within this simulator, different abstraction techniques are used to tackle the state-explosion problem. A case study shows the applicability of this approach.