Design and implementation of automatic verification for PLC systems

Programmable Logic Controller (PLC) have been widely used in industries, and safety and reliability of them has been urgently concerned. However, it´s hard to verify all the cases to discover the logical flaws of complex systems by traditional testing. Formal verification methods introduce mathematical rigor in their analysis thereby guaranteeing exhaustive state space coverage. But there is not an effective and efficient tool for PLC verification, and the general-purpose formal tools need lots of relevant knowledge. This paper proposes an automatic verification tool for PLC systems. It includes graphical modeling, syntax check, code generation, code optimization and representation of the counter-examples which violate some system properties.