资源描述：
《基于形式化方法的PLC建模和检测-毕业论文外文文献翻译》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。
1、外文文献译文设计(论文)题目:S7-200系列PLC实现电梯模型控制专业与班级:学生姓名:指导教师:年月日10J.SoftwareEngineering&Applications,2010,3,1054-1059doi:10.4236/jsea.2010.311124PublishedOnlineNovember2010(http://www.SciRP.org/journal/jsea)CopyrightPLCModelingandCheckingBasedonFormalMethod*YueshanZheng1,2,GuimingLuo1,2,JunboSun1
2、,2,JunjieZhang1,2,ZhenfengWang1,21TsinghuaNationalLaboratoryforInformationScienceandTechnology,TsinghuaUniversity,Beijing,China;2SchoolofSoftware,TsinghuaUniversity,Beijing,China.Email:championkop@gmail.com,gluo@tsinghua.edu.cnReceivedSeptember5th,2010;revisedSeptember16th,2010;accepte
3、dSeptember24th,2010.ABSTRACTHighreliabilityisthekeytoperformanceofelectricalcontrolequipment.PLCcombinescomputertechnology,automaticcontroltechnologyandcommunicationtechnologyandbecomeswidelyusedforautomationofindustrialprocesses.SomerequirementsofcomplexPLCsystemscannotbesatisfiedbyth
4、etraditionalverificationmethods.Inthispaper,anefficientmethodforthePLCsystemsmodelingandverificationisproposed.Toensurethehigh-speedpropertyofPLC,weproposedatechniqueof“Timeintervalmodel”and“notice-waiting”.ItcouldreducethestatespaceandmakeitpossibletoverifysomecomplexPLCsystems.Also,t
5、heconversionfromthebuiltPLCmodeltothePROMALlanguageisobtainedandatoolPLC-CheckerformodelingandcheckingPLCsystemsaredesigned.UsingPLC-CheckertocheckaclassicalPLCexample,acounter-exampleisfound.Althoughtheprobabilityofthislogicerroroccursverysmall,itcouldresultinsystemcrashfatally.Keywor
6、ds:ModelChecking,PLCModeling,PLC-Checker,FormalMethod1.IntroductionPLCisanautomaticcontroldevicethatcanreceiveinformationfromsensors,computingdeviceorotherPLClogicinputsignal,andoutputthelogicsignalprocessed.Thecontrolalgorithmcanbewrittenusingstandardlanguage,suchasLadderDiagram(LD),S
7、tructuredText(ST)orInstruction10List(IL)[1].ThetechniqueofPLCusingprogrammablelanguagetocontrollargescaleintegratedcircuithasbeenwidelyusedinindustry[2].Becauseofsafetycriticalsoftwarecancauseseriousdamagetolifeorproperty,verificationofsafetycriticalsoftwarehasbecomeanindispensablest
