计算机系统应用
計算機繫統應用
계산궤계통응용
APPLICATIONS OF THE COMPUTER SYSTEMS
2014年
9期
198-203
,共6页
王芳芳%雷建和%张丹%聂余满%高志
王芳芳%雷建和%張丹%聶餘滿%高誌
왕방방%뢰건화%장단%섭여만%고지
形式化方法%信号解释Petri网%模型检测%机器人焊接单元
形式化方法%信號解釋Petri網%模型檢測%機器人銲接單元
형식화방법%신호해석Petri망%모형검측%궤기인한접단원
formal methods%Signal Interpreted Petri Net%model checking%robot welding unit
针对传统的PLC编程方式在解决复杂控制问题时存在的缺陷,采用一种将形式化和信号解释Petri网(SIPN)应用于PLC程序设计的方法。通过一个机器人焊接单元的例子来说明这一设计过程,首先建立系统控制算法的信号解释Petri网模型,验证其是否满足基本Petri网的安全性、活性和可逆性的特征,然后利用模型检测工具Cadence SMV对系统模型进行验证和确认(V&V),检验其是否满足SIPN的确定性、终止性和输出正确性,从而避免了控制算法的设计过程中可能出现的并发、冲突和死锁等事件,由此设计出具有更高的正确性和可靠度的PLC程序。
針對傳統的PLC編程方式在解決複雜控製問題時存在的缺陷,採用一種將形式化和信號解釋Petri網(SIPN)應用于PLC程序設計的方法。通過一箇機器人銲接單元的例子來說明這一設計過程,首先建立繫統控製算法的信號解釋Petri網模型,驗證其是否滿足基本Petri網的安全性、活性和可逆性的特徵,然後利用模型檢測工具Cadence SMV對繫統模型進行驗證和確認(V&V),檢驗其是否滿足SIPN的確定性、終止性和輸齣正確性,從而避免瞭控製算法的設計過程中可能齣現的併髮、遲突和死鎖等事件,由此設計齣具有更高的正確性和可靠度的PLC程序。
침대전통적PLC편정방식재해결복잡공제문제시존재적결함,채용일충장형식화화신호해석Petri망(SIPN)응용우PLC정서설계적방법。통과일개궤기인한접단원적례자래설명저일설계과정,수선건립계통공제산법적신호해석Petri망모형,험증기시부만족기본Petri망적안전성、활성화가역성적특정,연후이용모형검측공구Cadence SMV대계통모형진행험증화학인(V&V),검험기시부만족SIPN적학정성、종지성화수출정학성,종이피면료공제산법적설계과정중가능출현적병발、충돌화사쇄등사건,유차설계출구유경고적정학성화가고도적PLC정서。
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.