资源描述：
《形式化方法和信号解释petri网在plc编程中的应用①》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。
1、计算机系统应用http://www.c-s-a.org.cn2014年第23卷第9期形式化方法和信号解释Petri网在PLC编程中的应用①11231王芳芳,雷建和,张丹,聂余满,高志1(青岛理工大学自动化工程学院,青岛266033)2(安大略理工大学工程及应用科学学院,奥沙瓦L1H7K4)3(中科院合肥智能机械研究所,合肥230031)摘要:针对传统的PLC编程方式在解决复杂控制问题时存在的缺陷,采用一种将形式化和信号解释Petri网(SIPN)应用于PLC程序设计的方法.通过一个机器人焊接单元的例子来说明这一设计过程,首先建立系统控制算法的信号解释Petri网模型,验证
2、其是否满足基本Petri网的安全性、活性和可逆性的特征,然后利用模型检测工具CadenceSMV对系统模型进行验证和确认(V&V),检验其是否满足SIPN的确定性、终止性和输出正确性,从而避免了控制算法的设计过程中可能出现的并发、冲突和死锁等事件,由此设计出具有更高的正确性和可靠度的PLC程序.关键词:形式化方法;信号解释Petri网;模型检测;机器人焊接单元ApplicationofFormalMetrodsandSignalInterpretedPetriNettoPLCProgramming11231WANGFang-Fang,LEIJian-He,ZHANGDan
3、,NIEYu-Man,GAOZhi1(SchoolofAutomation,QingdaoTechnologicalUniversity,Qingdao266033,China)2(SchoolofEngireeringandAppliedSciences,UniversityofOntarioInstituteTechnology,OshawaL1H7K4,Canada)3(InstituteofIntelligentMachines,ChineseAcademyofSciences,Hefei230031,China)Abstract:Toovercomethedef
4、ectsintraditionalPLCprogramming,anapproachcombinedformalmethodswithSignalInterpretedPetriNet(SIPN)ispresented.Anexampleofrobotweldingunitisusedtoillustratethisprocess.ThispaperbuildsamodelofthecontrolalgorithmwithSignalInterpretedPetriNetfirst,andverifieswhetheritsatisfiesthesafety,livene
5、ssandreversibilitycharacteristicsofbasicPetrinet.ThenitusesthemodelcheckingtoolCadenceSMVformodelverificationandvalidation,totestwhetheritmeetsthepropertiesofcertainty,terminationandoutputcorrectness.Thusthepossibleeventslikeconcurrency,conflictanddeadlockincontrolalgorithmdesigningproces
6、scanbeavoidedandcorrectanddependablePLCprogramsaredesigned.Keywords:formalmethods;SignalInterpretedPetriNet;modelchecking;robotweldingunit可编程控制器(PLC)功能强大、可靠性高、使用方(1)一般说来,传统的PLC程序设计是一个开环便,因此被广泛应用于工业制造和生产过程中.基于的过程,从程序的编程设计到调试运行工作量大,整传统的IEC61131-3标准中定义的逻辑控制设计语言如个开发工作周期长、成本高.梯形图(LD)、顺序功能图(SFC
7、)、功能块图(FB)等图形(2)当程序的运行出现错误时,设计者只能按照化语言,虽然程序指令形象直观,但指令间的逻辑关程序设计的顺序由上至下逐条检查,对程序检测的过系抽象,程序调试的过程较为复杂和繁琐.近年来,程不能进行反馈,不能很快指出问题具体出现在哪一随着控制系统复杂程度的不断提高和用户对安全性和部分.功能需求的不断增加,传统的PLC程序设计方法已不(3)PLC编程软件只能检测语法、语义上的错误,能满足要求,主要有如下几个弊端:并不能检测到逻辑上的问题,不能很好地解决系统中①基金项目:山东泰山学者建设工程基金(C2010-T
