Formal Modeling And Verification Of Motion Control Program Based On PLC

At present,programmable controller(PLC)has been widely used in the field of industrial control.The motion control system realized by PLC can use many kinds of languages,among which function block diagram(FBD)and ladder diagram(LD)are the programming languages commonly used in the field of industrial control and automation,but there is little verification for these two programming languages.Therefore,this paper aims to verify the credibility of the motion control program,and studies how to improve the credibility of the function block and the ladder diagram in combination with the major national issues,and puts forward the model conversion method for the PLCopen motion control function block and the ladder diagram,so as to verify the reliability of the motion control program.This paper focuses on the verification of function block diagram program and ladder diagram program,and makes the following research in program description and model transformation:1)According to the periodic scanning characteristic of PLC,this paper uses time automata as the modeling method,and proposes the cyclic execution model of PLC.This paper focuses on the research of function block diagram language and time automata model based on UPPAAL system.Aiming at the credibility of motion control system,this paper proposes a transition method(D-U transition)from function block diagram to UPPAAL system is proposed,which transforms function block diagram program into time automata model based on UPPAAL system.2)According to the International Standard IEC 61131-3,the ladder program is ed into Boolean expression and the colored Petri net model of the ladder program is established.In the ladder program of realizing motion control,by using timer to increase delay between two instructions,it can be used to ensure that two instructions enter the internal CPU of PLC in sequence.Therefore,this paper,established colored Petri net model for three different function timers.The function block diagram model and ladder diagram model are implemented and verified respectively.UPPAAL model checking tool is used to model and verify the transformation method from function block diagram to time automata.Through CPN tools automatic analysis tool and CPN ML syntax,the modeling method of colored Petri net based on ladder diagram is simulated and verified.The experimental results show that the function block diagram model and the ladder diagram model are reliable.Through the experimental results,developers can find the security problems or performance problems of programs or systems,so as to better improve the system.