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