三菱PLC立体车库毕业设计-本科毕业设计外文翻译

毕业设计外文文献翻译毕业设计题目 多车位轿车立体停车库PLC控制系统设计翻译题目专 业姓 名班 级学 号指导教师

可编程逻辑控制器机械设计制造及其自动化XXXA0916XXXXX机械与材料工程学院二O一四年四月可编程逻辑控制器PLC介绍PLCS（可编程逻辑控制器）是用于各种自动控制系统和过程的可控网络集PLCS备编程。I/OPLCSPLC括扫描时间，指令数量，数据存储和程序存储。扫描时间是PLCPLC软件（例如数学运算）数据存储是存储数据的能力。程序存储是控制软件的能力。用于可编程逻辑控制器的输入设备包括DC，AC，中间继电器，热电偶，RTD，频率或脉冲，晶体管和中断信号输入；输出设备包括DC，AC，继电器，中间继电器，频率或脉冲，晶体管，三端双向可控硅开关元件；PLC的编程设备包括控制面板，手柄和计算机。可编程逻辑控制器用各种软件编程语言来控制。这些语言包括顺序执行表（SFC，动作方块图（FBD，梯形图（L，结构文本（ST，指令序列I，继电器梯形图RICBasicIEC61131-3编程环境能支持五种语言，用国际标准加以规范，分别为SFC，FBD，LD，ST。这便允许了多卖主兼容性和多种语言编程。SFC是一种图表语言，它提供了编程顺序的配合，就能支持顺序选择和并列选择，二者择其一即可。FBD以与用户交流和接口运行相1 合LD是适用于离散控制和互锁逻辑的图表语言。FBDST程和计算，不太适用于图表语言。摘自：科学与工程期刊作者：LaurenceBodelotIL是与组合编码相似的低级语言。它用在相对比较简单的逻辑指令。继电C语言是一种高级编程语言，适用于处理最复杂的计算，连续的数据采集任务。PCBASIC语言是用于处理数据的连续的数字采集和接口运行的高级语言。可编程逻辑控制器也规范了许多计算机接口设备，网络规则和特色。PLC能源设备和运行环境也是非常重要的。指令对于简单的编程，继电器型PLC是有效的。随着功能的复杂化，复杂的PLC计算机一次只能执行一个指令，他们是这样运行的，尽管许多计算机看上去一次在做许多事情。正如图所示的计算机组成。图1简化个人计算机结构图（）2备的作用。2输入输出方向图（注意：大多数设计图表都是左）CPU之前，它穿过缓冲电路。CPU一个控制器，它通过在屏幕上输出激励和输入来自鼠标和键盘的响应来控制用户。PLC变成：输入设备—键盘与接近开关相类比。输入电路—24V—686CPUPLCCPU模块。输出电路—图形卡就像一个三相开关输出卡。输出设备—监控器就像指示灯。存储器—PLC的存储器与个人计算机的存储器相似。用普通个人计算机可以运行PLC，虽然则并不被提倡做。就PLC来说，输入和输出设备设计得更加可靠，更加粗糙，更适合恶劣的制造环境。运行顺序PLCPLC此时将从自我检测开始重新启动这个过程，这个过程很明显地每秒钟重复101003所示图3 PLC扫描循环自我检测—（如果在很PLC系统。—）输入扫描—PLC（PLC功能，能直接读取输入值，避免了输入表格。逻辑处理/扫描—基于存储器的输入表格，程序被一次执行一步，同时输出值也被修正，这是其它节的集中。输出扫描—输出表格从存储器复制到输出芯片，这些芯片然后驱动输出仪器。它可能在输入扫描之间会减少或者丢失。PLC最初被启动时，通常的输出会被关闭，这不会影响输入值。输入输出扫描PLCPLCPLC慢。逻辑扫描4所示，梯形图将按从左到右，从上到下的顺序被解释。在图中，梯形逻辑扫描将从最高层开始。在底层，它将先解释高层输出，然后输出它下面的分支。在第二层，沿着梯形逻辑图移动之前，将先解释分支。图4梯形图逻辑执行顺序5X1BX1，得到相XA相等。在逻辑扫描PLC状态显示

5错误重复输出PLCPLC前端通常有一定数量的状态指示灯。通常指示灯表明：电源启动—只要PLC带电，它将被启动。程序运行—这将指示是否程序正在运行或是否没有程序正在运行。错误显示—PLC有大的硬件或软件错误时，这将有显示。这些灯通常用于调试。一定数量的按钮也将提供给PLC的按钮是一个运行/编程选择开关，当在保持状态时，它将被调到编程；当在生PLC开关在前面。这需要被设计到系统剩余部分。PLC6所示。‗firstscan‘输入在梯形图被第一次扫描时，将是对的，而在其PL—5的‗first的地址是‗S21/14‘‗light‘，直到‗clear‘被启动。因此灯PLC‗clear‘scan模块在‗firstpass‘模块中被提到。存储器类型

6PLC有几种基本的现在经常使用的计算机存储器类型：RAM（随机存储器）—种不稳定存储器，每个PLCROM（只读存储器）—这种存储器是永久性的不可擦除的。它通常用于存放PLC的操作系统。EPROM（可擦除可编程只读存储器）—这是一种像ROM一样可编程的存储器，但是它能用紫外线光擦除并且可以重新编程。电可擦除可编程只读存储器ROMEPROM更加普遍。PLCRAMCPUROMPLC的基本操作系统。当有电时，RAM的内容被保存，但是问题在于当供给存储器的电源失去时会发生什么。原先PLCRAM不会丢失。这种方法现在仍被使用，但变得不那么受欢迎。EPROMS也是PLC编程的比较好的选择。EPROMPLCPLCPLC被EPROMPLC并且运行。这种方法非常可EEPROMPLC的永久部分，程序能EPROMPLC系统发生影响。检验和优化一个PLC控制时间表混合的系统是快速地成长的重要一个研究领域。在系统中出现不连续的和PLC和他们组成的系统语言都没有好VHS(混合的系统)有许多个案研究。其中一个研究为一个实验的化学工厂与PLC控制流程设PLC性质。基于软件的PLC系统PLC.从传感器中读取输入，式.例如，计算机正运行一个游戏，就可能减慢或停止计算机.这个以及其它问题现在正被研究，好的解决方案不久就会出现。概要PLC系统和计算机与输入设备，输出设备,存储器等很相似。PLC系统不断地执行系统检查，输入扫描,逻辑扫描和输出扫描这个循环。当逻辑图被扫描时，输入的变化没有被发现,输出也没有被修正。PLCRAMEPROM存放永久程序。实际问题一个PLC系统通常包括RAM，ROM，EPROM和/或电池吗？PLC的指示灯用于什么？为什么一个PLC系统每秒钟只能扫描梯形图几次？如果一个PLC系统的扫描时间比输入脉冲长，会发生什么?为什么？一个PLC系统与一部台式计算机的不同是什么？为什么PLC系统每次扫描要做自我检查？PLC检测时间会比简单程序所需时间长吗？实际问题解答每个PLC系统包括RAM和ROM，但是他们也包括EPROM或电池。诊断和保持。尽管程序是空的，PLC系统仍需扫描输入和输出，做自我检测。如果在两次输入扫描之间发生，脉冲就会丢失。PLC(PLC能够达到)有屏幕声音之类的输出设备，.取而代之，他们有电压,电流这样的输入设备和输出设备。PLC使用户为专门的任务设计程序,不常见的。这能帮助检测硬件和软件错误。如果一个错误发生了，PLC还继续运行,测则帮助检查出这些错误，并且安全地关闭系统。PLC1mms。ProgrammableLogicControllers(PLCs)1 AboutProgrammableLogicControllers(PLCs)PLCs(programmablelogiccontrollers)arethecontrolhubsforawidevarietyofautomatedsystemsandprocesses.Theycontainmultipleinputsandoutputsthatusetransistorsandothercircuitryto simulateswitchesandrelaysto controlequipment.Theyareprogrammableviasoftwareinterfacedviastandardcomputerinterfacesandproprietarylanguagesandnetworkoptions.ProgrammablelogiccontrollersI/Ochannelspecificationsincludetotalnumberofpoints,numberofinputsandoutputs,abilitytoexpand,andmaximumnumberofchannels. Numberofpointsisthesumoftheinputsandtheoutputs.PLCsmaybespecifiedbyanypossiblecombinationofthesevalues. Expandableunitsmaystackedorlinkedtogethertoincreasetotalcontrolcapacity. Maximumnumberchannelsreferstothemaximumtotalnumberofinputandoutputchannelsinanexpandedsystem. PLCsystemspecificationstoconsiderincludescantime,numberofinstructions,datamemory,andprogrammemory. ScantimeisthetimerequiredbythePLCtocheckthestatesofitsinputsandoutputs. Instructionsarestandardoperations(suchasmathfunctions)availabletoPLCsoftware. Datamemoryisthecapacityfordatastorage. Programmemoryisthecapacityforcontrolsoftware.AvailableinputsforprogrammablelogiccontrollersincludeDC,AC,analog,thermocouple,RTD,frequencyorpulse,transistor,andinterruptinputs.OutputsforPLCsincludeDC,AC,relay,analog,frequencyorpulse,transistor,andtriac.ProgrammingoptionsforPLCsincludefrontpanel,handheld,andcomputer.Programmable logic controllers use a variety of software programminglanguagesforcontrol.TheseincludeIEC61131-3,sequentialfunctionchart(SFC),functionblockdiagram(FBD),ladderdiagram(LD),structuredtext(ST),instructionlist(IL),relayladderlogic(RLL),flowchart,C,andBasic. TheIECprogrammingenvironmentprovidessupportforfivelanguagesspecifiedbytheglobalstandard:SequentialFunctionChart,FunctionBlockDiagram,LadderDiagram,StructuredText,andInstructionList.Thisallowsformulti-vendorcompatibilityandmulti-language programming. SFC is a graphical language that providescoordinationofprogramsequences,supportingalternativesequenceselectionsandparallelsequences. FBDusesabroadfunctionlibrarytobuildcomplexproceduresinagraphicalformat.Standardmathandlogicfunctionsmaybecoordinatedwithcustomizablecommunicationandinterfacefunctions. LDisagraphiclanguagefordiscretecontrolandinterlockinglogic.ItiscompletelycompatiblewithFBDfordiscretefunctioncontrol. STisatextlanguageusedforcomplexmathematicalproceduresandcalculationslesswellsuitedtographicallanguages. ILisalow-levellanguagesimilartoassemblycode. Itisusedinrelativelysimplelogicinstructions. RelayLadderLogic(RLL),orladderdiagrams,istheprimaryprogramminglanguageforprogrammablelogiccontrollers(PLCs).logicprogrammingisagraphicalrepresentationoftheprogramdesignedtolooklikerelaylogic. FlowChartisagraphicallanguagethatdescribessequentialoperationsinacontrollersequenceorapplication.Itisusedtobuildmodular,reusablefunctionlibraries. Cisahighlevelprogramminglanguagesuitedtohandlethemostcomplexcomputation, sequential, anddatalogging tasks. Itis typically developed anddebuggedonaPC. BASICisahighlevellanguageusedtohandlemathematical,sequential,datacapturingandinterfacefunctions.Programmablelogiccontrollerscanalsobespecifiedwithanumberofcomputerinterfaceoptions,networkspecificationsandfeatures.PLCpoweroptions,mountingoptionsandenvironmentaloperatingconditionsareallalsoimportanttoconsider.INTRODUCTIONForsimpleprogrammingtherelaymodelofthePLCissufficient.AsmorecomplexfunctionsareusedthemorecomplexVonNeumanmodelofthePLCmustbeused.AVonNeumancomputerprocessesoneinstructionatatime.Mostcomputersoperatethisway,althoughtheyappeartobedoingmanythingsatonce.ConsiderthecomputercomponentsshowninFigure1.Figure1SimplifiedPersonalComputerArchitectureInputisobtainedfromthekeyboardandmouse,outputissenttothescreen,andthediskandmemoryareusedforbothinputandoutputforstorage.(Note:thedirectionsofthesearrowsareveryimportanttoengineers,alwayspayattentiontoindicatewhereinformationisflowing.)ThisfigurecanberedrawnasinFigure2toclarifytheroleofinputsandoutputs.Figure2 AnInput-OutputOrientedArchitectureInthisfigurethedataenterstheleftsidethroughtheinputs.(Note:mostengineeringdiagramshaveinputsontheleftandoutputsontheright.)IttravelsthroughbufferingcircuitsbeforeitenterstheCPU.TheCPUoutputsdatathroughothercircuits.Memoryanddisksareusedforstorageofdatathatisnotdestinedforoutput.Ifwelookatapersonalcomputerasacontroller,itiscontrollingtheuserbyoutputtingstimulionthescreen,andinputtingresponsesfromthemouseandthekeyboard.APLCisalsoacomputercontrollingaprocess.Whenfullyintegratedintoanapplicationtheanalogiesbecome;inputs-thekeyboardisanalogoustoaproximityswitchinput-circuits-theserialinputchipislikea24Vdcinputcardcomputer-the686CPUislikeaPLCCPUunitoutput-circuits-agraphicscardislikeatriacoutputcardoutputs-amonitorislikealightstorage-memoryinPLCsissimilartomemoriesinpersonalcomputersItisalsopossibletoimplementaPLCusinganormalPersonalComputer,althoughthisisnotadvisable.InthecaseofaPLCtheinputsandoutputsaredesignedtobemorereliableandruggedforharshproductionenvironments.OPERATIONSEQUENCEAllPLCshavefourbasicstagesofoperationsthatarerepeatedmanytimespersecond.Initiallywhenturnedonthefirsttimeitwillcheckit‘sownhardwareandsoftwareforfaults.Iftherearenoproblemsitwillcopyalltheinputandcopytheirvaluesintomemory,thisiscalledtheinputscan.Usingonlythememorycopyoftheinputstheladderlogicprogramwillbesolvedonce,thisiscalledthelogicscan.Whilesolvingtheladderlogictheoutputvaluesareonlychangedintemporarymemory.Whentheladderscanisdonetheoutputswillbeupdatedusingthetemporaryvaluesinmemory,thisiscalledtheoutputscan.ThePLCnowrestartstheprocessbystartingaselfcheckforfaults.Thisprocesstypicallyrepeats10to100timespersecondasisshowninFigure3.Figure3 PLCScanCycleSELFTEST-Checkstoseeifallcardserrorfree,resetwatch-dogtimer,etc.(Awatchdogtimerwillcauseanerror,andshutdownthePLCifnotresetwithinashortperiodoftime-thiswouldindicatethattheladderlogicisnotbeingscannednormally).INPUTSCAN-Readsinputvaluesfromthechipsintheinputcards,andcopiesvaluesmemory.ThismakesthePLCoperationfaster,andavoidscaseswhereaninputchangesfromthestarttotheendoftheprogram(e.g.,anemergencystop).TherearespecialPLCfunctionsthatreadtheinputsdirectly,andavoidtheinputtables.LOGICSOLVE/SCAN-Basedontheinputtableinmemory,theprogramisexecuted1stepatatime,andoutputsareupdated.Thisisthefocusofthelatersections.OUTPUTSCAN-Theoutputtableiscopiedfrommemorytotheoutputchips.Thesechipsthendrivetheoutputdevices.Theinputandoutputscansoftenconfusethebeginner,buttheyareimportant.Theinputscantakesasnapshotoftheinputs,andsolvesthelogic.Thispreventspotentialproblemsthatmightoccurifaninputthatisusedinmultipleplacesintheladderlogicprogramchangedwhilehalfwaythroughaladderscan.Thuschangingthebehaviorsofhalfoftheladderlogicprogram.Thisproblemcouldhavesevereeffectsoncomplexprogramsthataredevelopedlaterinthebook.Onesideeffectoftheinputscanisthatifachangeininputistooshortinduration,itmightfallbetweeninputscansandbemissed.WhenthePLCisinitiallyturnedonthenormaloutputswillbeturnedoff.Thisdoesnotaffectthevaluesoftheinputs.TheInputandOutputScansWhentheinputstothePLCarescannedthephysicalinputvaluesarecopiedintomemory.WhentheoutputstoaPLCarescannedtheyarecopiedfrommemorytothephysicaloutputs.Whentheladderlogicisscanneditusesthevaluesinmemory,nottheactualinputoroutputvalues.Theprimaryreasonfordoingthisissothatifaprogramusesaninputvalueinmultipleplaces,achangeintheinputvaluewillnotinvalidatethelogic.Also,ifoutputbitswerechangedaseachbitwaschanged,insteadofallatonceattheendofthescanthePLCwouldoperatemuchslower..2 TheLogicScanLadderlogicprogramsaremodelledafterrelaylogic.Inrelaylogiceachelementintheladderwillswitchasquicklyaspossible.Butinaprogramelementscanonlybeexaminesoneatatimeinafixedsequence.ConsidertheladderlogicinFigure4,theladderlogicwillbeinterpretedleft-to-right,top-to-bottom.Inthefiguretheladderlogicscanbeginsatthetoprung.Attheendoftherungitinterpretsthetopoutputfirst,thentheoutputbranchedbelowit.Onthesecondrungitsolvesbranches,beforemovingalongtheladderlogicrung.Figure4LadderLogicExecutionSequenceThelogicscansequencebecomeimportantwhensolvingladderlogicprogramswhichuseoutputsasinputs.ItalsobecomesimportantwhenconsideringoutputConsiderFigure5,thefirstlineofladderlogicwillexamineinput AandsetoutputXtohavethesamevalue.Thesecondlinewillexamineinput BandsettheoutputXtohavetheoppositevalue.SothevalueofXwasonlyequaltoAuntilthesecondlineofladderlogicwasscanned.Recallthatduringthelogicscantheoutputsareonlychangedinmemory,theactualoutputsareonlyupdatedwhentheladderlogicscaniscomplete.Thereforetheoutputscanwouldupdatetherealoutputsbaseduponthesecondlineofladderlogic,andthefirstlineofladderlogicwouldbeineffective.Figure5 ADuplicatedOutputErrorPLCSTATUSThelackofkeyboard,andotherinput-outputdevicesisverynoticeableonaPLC.OnthefrontofthePLCtherearenormallylimitedstatuslights.Commonlightsindicate;poweron-thiswillbeonwheneverthePLChaspowerprogramrunning-thiswilloftenindicateifaprogramisrunning,orifnoprogramisrunningfault-thiswillindicatewhenthePLChasexperiencedamajorhardwareorsoftwareproblem.Theselightsarenormallyusedfordebugging.LimitedbuttonswillalsobeprovidedforPLChardware.Themostcommonwillbearun/programswitchthatwillbeswitchedtoprogramwhenmaintenanceisbeingconducted,andbacktorunwheninproduction.ThisswitchnormallyrequiresakeytokeepunauthorizedpersonnelfromalteringthePLCprogramorstoppingexecution.APLCwillalmostneverhaveanon-offswitchorresetbuttononthefront.Thisneedstobedesignedintotheremainderofthesystem.ThestatusofthePLCcanbedetectedbyladderlogicalso.Itiscommonforprogramstochecktoseeiftheyarebeingexecutedforthefirsttime,asshowninFigure6.The‘firstscan‘inputwillbetrueontheveryfirsttimetheladderlogicisscanned,butfalseoneveryotherscan.Inthiscasetheaddressfor‘firstscan‘inaPLC-5is‘S2:1/14‘.Withthelogicintheexamplethefirstscanwillsealon‘light‘,until‘clear‘isturnedon.SothelightwillturnonafterthePLChasbeenturnedon,butitwillturnoffandstayoffafter‘clear‘isturnedon.The‘firstscan‘bitisalsoreferredtoatthe‘firstpass‘bit.Figure6 AnprogramthatchecksforthefirstscanofthePLCMEMORYTYPESThereareafewbasictypesofcomputermemorythatareinusetoday.RAM(RandomAccessMemory)-thismemoryisfast,butitwillloseitscontentswhenpowerislost,thisisknownasvolatilememory.EveryPLCusesthismemoryforthecentralCPUwhenrunningthePLC.ROM(ReadOnlyMemory)-thismemoryispermanentandcannotbeerased.ItisoftenusedforstoringtheoperatingsystemforthePLC.EPROM(ErasableProgrammableReadOnlyMemory)-thisismemorythatcanbeprogrammedtobehavelikeROM,butitcanbeerasedwithultravioletlightandreprogrammed.EEPROM(ElectronicallyErasableProgrammableReadOnlyMemory)–ThismemorycanstoreprogramslikeROM.Itcanbeprogrammedanderasedusingavoltage,soitisbecomingmorepopularthanEPROMs.AllPLCsuseRAMfortheCPUandROMtostorethebasicoperatingsystemforthePLC.WhenthepowerisonthecontentsoftheRAMwillbekept,buttheiswhathappenswhenpowertothememoryislost.OriginallyPLCvendorsusedRAMwithabatterysothatthememorycontentswouldnotbelostifthepowerwaslost.Thismethodisstillinuse,butislosingfavor.EPROMshavealsobeenapopularchoiceforprogrammingPLCs.TheEPROMisprogrammedoutofthePLC,andthenplacedinthePLC.WhenthePLCisturnedontheladderlogicprogramontheEPROMisloadedintothePLCand run.Thismethodcanbevery reliable,buttheerasingandprogrammingtechniquecanbetimeconsuming.EEPROMmemoriesareapermanentpartofthePLC,andprogramscanbestoredinthemlikeEPROM.Memorycostscontinuetodrop,andnewertypes(suchasflashmemory)arebecomingavailable,andthesechangeswillcontinuetoimpactPLCs.VerificationandoptimizationofaPLCcontrolscheduleTheverificationofhybridsystemsisaresearchareaofrapidlygrowingimportanceintheformalmethodscommunity.Thepresenceofbothdiscreteandcontinuousphenomenainsuchsystemsposesaninspiringchallengeforourspecificationandmodellingtechniques,aswellasforouranalyticcapacities.Thishasledtothedevelopmentofnew,expressivemodels,suchastimedandhybridautomata,andnewverificationmethods,mostnotablymodelcheckingtechniquesinvolvingasymbolictreatmentofreal-time(andhybrid)aspects.Animportantexampleofhybrid(embedded)systemsareprocesscontrolprograms,whichinvolvethedigitalcontrolofprocessingplants,e.g.,chemicalplants.Aclassofprocesscontrollers that are of considerable practical importance are those that areimplementedusingProgrammableLogicControllersorPLC.Unfortunately,bothPLCandtheirassociatedprogramminglanguageshavenowell-definedformalmodelsorsemantics,whichcomplicatesthedesignofreliablecontrollersandtheiranalysis.Toassessthecapacityofstate-of-the-art formalmethodsandtoolsfortheanalysisofhybridsystems,theEUresearchprojectVHS(VerificationofHybridSystems)hasdefinedanumberofcasestudies.OneofthesestudiesconcernsthedesignandverificationofaPLCprogramforanexperimentalchemicalplant.Inthisarticlewereportontheuseoftwomodelcheckersfortheverificationofaprocesscontrolprogramforthegivenplantandthederivationofoptimalcontrolschedules.Itisacompanionpaperto,whichconcentratesonthecorrectdesignoftheprocesscontroller.Theoriginalintentionofourapproachwastoseehowmuchcouldbeachievedusingthestandardmodelchecking environmentofSPIN/Promela.Asthesymboliccalculationsofreal-timemodelcheckerscanbequiteexpensiveitisinterestingtotryandexploittheefficiencyofestablishednon-real-timemodelcheckerslikeSPINinthosecaseswherepromisingwork-aroundsseemtoexist.Incasewehandledtherelevantreal-timepropertiesofthePLCcontrollerusingatime-abstractiontechnique;fortheschedulingweimplementedinPromelaaso-calledvariabletimeadvanceprocedure.Forthiscasestudythesetechniquesprovedsufficienttoverifythedesignofthecontrollerandderive(time-)optimalscheduleswithveryreasonabletimeandspacerequirements.Afirstreportonourexperienceshasbeenpublishedas,whosefindingsarefurtherextendedandelaboratedinthisarticle.Oneoftheconclusionsofourinitialexperimentsasreportedintheinitialpublicationwasthat―...itwouldbeusefultobeabletoinfluencethesearchstrategyofthemodelcheckermoredirectlyandguidethesearchfirstintothoseparts...wherecounterexamplesarelikelytobefound.‖Sincethispublicationanewversionofthereal-timemodelcheckingtoolUPPAALhasbecomeavailablethatemploysacost-guided evaluation strategy for state-space exploration, viz., UPPAAL.Thistoolisanaturalcandidatetosupportthederivationofoptimalcontrolschedulesinareal-timeenvironment.Thismotivatedustocarryouttheoptimizationpartofthecasestudyagainwithcost-optimalUPPAAL,bothasaninterestingexerciseinitsownright,andtocollectdatatointerpretandcomparewiththeresultsobtainedwithSPIN.Therestofthispaperisorganizedasfollows:Sect.2givesadescriptionofthebatchplant,thenatureofPLC,andadescriptionofthecontrolprogramthatwassystematicallydesignedinpreviouswork.Section3describesthePromelamodelsfortheplantandthecontrolprocess,andtheiruseforitsformalverificationandoptimization.Section4thenintroducesacost-optimalUPPAALmodelofthesameprocesses,andpresentstheoptimizationresultsthatwereobtainedusingit.Section5,finally,evaluatestheworkandpresentsourconclusions.SOFTWAREBASEDPLCSThedroppingcostofpersonalcomputersisincreasingtheiruseincontrol,includingthereplacementofPLCs.Softwareisinstalledthatallowsthepersonalcomputertosolveladderlogic,readinputsfromsensorsandupdateoutputstoactuators.Theseareimportanttomentionherebecausethey