Formal Modelling And Verification Of PLCopen Motion Control Function Blocks

The internal operations of the Motion Control function blocks are more complex than the standard function blocks of programmable controller,and there are rare traditional methods address this type of function blocks.This paper proposed a verification method for PLCopen Motion Control function blocks.This method are divided into three aspects:function block structure modeling,motion control engine modeling and transformation method description.And then,this method will be applied to a sample program.After the verification procedure,the experiment results show that this method can effectively verify functional features and performance characteristics of a system.For functional block structure modeling part,this paper designs a functional block diagram program model,which makes a unified abstraction of standard function blocks,motion control function blocks,functions and variables.For transformation part,this paper designs a transformation algorithm to translate the function block diagram program model into an automaton model based on Uppaal tool.The motion control engine model is implemented by a priced timed automaton,which takes into account physical system attributes and time characteristic.This model extends the transitions of an automaton to the transitions with weight.This model expresses the continuous quantities such as displacement and velocity in discrete quantities and focuses on the real-time aspect of the system.This paper uses the presented method to verify the security,reachability and realtime properties of the system.The verification results will be useful for the developers who want to improve the system.This modeling method for the PLCopen Motion Control function blocks can be used as the reference for the modeling of the other function blocks with complex operations.