本文已被：浏览 2022次 下载 3871次
Received:January 04, 2014 Revised:March 17, 2014
Received:January 04, 2014 Revised:March 17, 2014
中文摘要: 针对传统的PLC 编程方式在解决复杂控制问题时存在的缺陷，采用一种将形式化和信号解释Petri 网(SIPN)应用于PLC 程序设计的方法. 通过一个机器人焊接单元的例子来说明这一设计过程，首先建立系统控制算法的信号解释Petri 网模型，验证其是否满足基本Petri 网的安全性、活性和可逆性的特征，然后利用模型检测工具Cadence SMV 对系统模型进行验证和确认(V&V)，检验其是否满足SIPN 的确定性、终止性和输出正确性，从而避免了控制算法的设计过程中可能出现的并发、冲突和死锁等事件，由此设计出具有更高的正确性和可靠度的PLC 程序.
中文关键词: 形式化方法 信号解释Petri 网 模型检测 机器人焊接单元
Abstract:To overcome the defects in traditional PLC programming, an approach combined formal methods with Signal Interpreted Petri Net (SIPN) is presented. An example of robot welding unit is used to illustrate this process. This paper builds a model of the control algorithm with Signal Interpreted Petri Net first, and verifies whether it satisfies the safety, liveness and reversibility characteristics of basic Petri net. Then it uses the model checking tool Cadence SMV for model verification and validation, to test whether it meets the properties of certainty, termination and output correctness. Thus the possible events like concurrency, conflict and deadlock in control algorithm designing process can be avoided and correct and dependable PLC programs are designed.
文章编号： 中图分类号： 文献标志码：
基金项目:山东泰山学者建设工程基金（C2010-T005）；国家自然科学基金（61201400）
引用文本：
王芳芳,雷建和,张丹,聂余满,高志.形式化方法和信号解释Petri 网在PLC 编程中的应用.计算机系统应用,2014,23(9):198-203
WANG Fang-Fang,LEI Jian-He,ZHANG Dan,NIE Yu-Man,GAO Zhi.Application of Formal Metrods and Signal Interpreted Petri Net to PLC Programming.COMPUTER SYSTEMS APPLICATIONS,2014,23(9):198-203
王芳芳,雷建和,张丹,聂余满,高志.形式化方法和信号解释Petri 网在PLC 编程中的应用.计算机系统应用,2014,23(9):198-203
WANG Fang-Fang,LEI Jian-He,ZHANG Dan,NIE Yu-Man,GAO Zhi.Application of Formal Metrods and Signal Interpreted Petri Net to PLC Programming.COMPUTER SYSTEMS APPLICATIONS,2014,23(9):198-203
