论文提出了一个针对PLCopen运动控制功能块的验证方法。相比于可编程控制器的标准功能块,运动控制功能块的内部实现更为复杂,并且缺少针对对该类型功能块的验证方法。论文提出的验证方法在文中被分为功能块结构建模、运动控制引擎建模和模型转换三个方面进行阐述,并在最后使用该方法对一个示例程序进行建模,再对验证后的结果进行分析。实验结果证明该方法可以有效的验证程序的部分功能特征和性能特征。对于功能块结构建模,文章设计了功能块图程序模型,对标准功能块、运动控制功能块、函数以及变量做了统一的抽象。对于模型转换,文章设计了转换算法,将功能块图程序模型转换成基于Uppaal系统的时间自动机模型。运动控制引擎模型采用加权时间自动机实现。模型统筹考虑了系统的物理属性和时间特性,并将系统内部状态的转换拓展为带权重的转换。此外,该模型将位移、速度等连续量以离散量表示,并重点突出了系统的实时性。在实验中,文章使用该模型验证了系统的安全性、可达性以及实时性。通过实验结果,开发人员可以发现程序或系统的安全性问题或性能改进点,从而更好地改进系统。文中针对PLCopen运动控制功能块的分析及建模方法可以为对其它的复杂功能块的分析、建模提供参考。