Cycle-bounded model checking of PLC software via dynamic large-block encoding
Dimitri Bohlender, Daniel S. Hamm, Stefan Kowalewski · 2018
Bounded model checking is a formal verification technique for checking reachability of unwanted behaviour within a bounded number of steps. In the context of PLC software, specifications treat the whole program as a single step, only considering the controller's observable state at the end of an execution-cycle. For a program containing loops, standard approaches will characterise shorter steps, losing the relation to the original bound, or try to unroll the loops statically.