形式化方法和信号解释Petri网在PLC编程中的应用

摘要：

针对传统的PLC编程方式在解决复杂控制问题时存在的缺陷，采用一种将形式化和信号解释Petri网(SIPN)应用于PLC程序设计的方法。通过一个机器人焊接单元的例子来说明这一设计过程，首先建立系统控制算法的信号解释Petri网模型，验证其是否满足基本Petri网的安全性、活性和可逆性的特征，然后利用模型检测工具Cadence SMV对系统模型进行验证和确认(V&V)，检验其是否满足SIPN的确定性、终止性和输出正确性，从而避免了控制算法的设计过程中可能出现的并发、冲突和死锁等事件，由此设计出具有更高的正确性和可靠度的PLC程序。

关键词：形式化方法、信号解释Petri网、模型检测、机器人焊接单元

分类号：TN9;TP3

资助基金：山东泰山学者建设工程基金C2010-T005;国家自然科学基金61201400

在线出版日期：2014-09-30（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：198-203