PLCopen标准库描述了常见的运动控制功能块,广泛运用于运动控制系统。不过,很少有方法来验证基于这个标准的系统。以验证运动控制程序的安全性、可达性为目标,提出针对PLCopen运动控制功能块的模型转换方法。根据可编程控制器的周期扫描特性,提出可编程控制器执行模型。提出将功能块图程序(function block diagram,FBD)转换为基于Uppaal系统的时间自动机模型,从而验证运动控制程序的可靠性。