Find in Library
Search millions of books, articles, and more
Indexed Open Access Databases
Toward Reliable Programmable Logic Controller Function Block Diagrams
oleh: Jianyong Zhao, Zhe Tao
Format: | Article |
---|---|
Diterbitkan: | IEEE 2021-01-01 |
Deskripsi
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.