Toward Reliable Programmable Logic Controller Function Block Diagrams

Programmable logic controllers (PLCs) are widely used in industrial electronic systems. With the augmenting complexity of system, the reliability poses a crucial challenge in safety critical applications. This paper proposes a formal modeling and verification approach for programming function block diagrams. Function block diagrams are formalized in a logic specification system. We consider the equivalence checking problem which occurs frequently between design implementations under different performance constraints. We present a novel method to harness a powerful co-induction proof strategy with bisimulation to establish the equivalence in a higher-order logic theorem proving system. We validate the effectiveness of our approach by a real industry application example with key scenarios. The soundness and the completeness of our approach are substantiated.