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

Modeling and verification of timed automata based on PLCopen motion control function block

作　　者：孙青怡 黄志韬 SUN Qing-yi;HUANG Zhi-tao

机构地区：[1]杭州电子科技大学计算机学院,杭州310018

出　　处：《制造业自动化》2021年第9期45-49,共5页Manufacturing Automation

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

关 键 词：PLCopen运动控制功能块 时间自动机 UPPAAL 

分 类 号：TP202[自动化与计算机技术—检测技术与自动化装置]