Symbolic verification of PLC safety-applications based on PLCopen automata
Dimitri Bohlender, Simon, Hendrik, Stefan Kowalewski · RWTH Publications (RWTH Aachen) · 2016
This paper presents a technique for verifying a PLC program’s compliance with respect to the automaton-based specifications used by the PLCopen. While related approaches only support a subset of expressible PLCopen automata and struggle with the state explosion problem, our technique both enables the logical characterisation of any PLCopen automaton and facilitates the verification of programs previously entailing exhaustive state space exploration and time outs. To enable fully symbolic reasoning we utilise the Property Directed Reachability capabilities of the Z3 SMT solver.