Design and Verification on the PLC Program Based on Formal Methods
Xue-Kun Chen · Journal of Huaqiao University · 2013
From the perspective of formal methods,this paper states lots of researches on the formal design and verification of programmable logic controllers(PLC) programs.As for formal design,the proposed methods,which are to judge whether PLC programs are correct and reliable based on Petri nets or automata,are depicted.As for formal verification,it is summarized that how to model PLC programs as Petri nets,and how to verify PLC programs using NuSMV or UPPAAL.At last,the advantages and disadvantages of these reported approaches are stated,and the research directions which are expected to breakthrough,are pointed out.