论文部分内容阅读
针对PLCopen运动控制系统安全验证问题，对PLCopen标准运动控制功能块语言、系统运动状态关系等方面进行了研究，提出一种新的分层描述时间自动机模型。该模型将系统程序状态与系统状态分别抽象定义，通过UP-PAAL验证器进行验证，以状态路径正确或错误转换作为系统可靠的分析结果，从而实现系统的逻辑安全验证。实验结果证明该方法可以完成PLCopen标准运动控制系统的逻辑安全验证，并且有效减少了模型转换的出错率。