基于PLCopen运动控制功能块的时间自动机建模与验证

摘要

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