A PLC Program Synthesis Method And The Proof Of Its Correctness

PLC(Programmable Logic Controller)is widely used in the field of industrial control.In safety-critical areas,the traditional manual programming method cannot guarantee the correctness of the PLC program.However,most of the existing research in the field of automatic code generation The automatically generated control program is difficult to understand and maintain,which seriously hinders the acceptance of the automatic generation of the control program by the industry.Among the existing automatic PLC program generation methods,the structured generation method produces the most understandable and maintainable results.However,the existing structured generation method has the following shortcomings:(1)Both the determinization of statutes and the checking of statute conflicts require constraint solving,which has a high time complexity.(2)The proof process of the automatic generation algorithm has not been verified by the machine.(3)It can only process timing specifications,not real-time specifications.The main work of this paper is as follows:(1)According to the need of formal description of PLC user specification,this paper improves and expands the existing specification pattern description language,and puts forward the real-time specification description language RTSPS4 PLC,and gives the formal description of its syntax and semantics.(2)By setting the priority between the specification item and the control object,a simple and unified specification conflict processing method is provided,and the link of finding conflict through constraint solution is avoided.On this basis,the algorithm S2 P of structured automatic generation PLC program is given.(3)The inductive proof method is adopted to prove that the RTSPS4 PLC specification after setting the priority,in the case of no cyclic dependence,the result generated by S2 P algorithm must be correct.The interactive theorem proving tool COQ is used to verify the correctness of S2 P algorithm.