Research On Modeling And Verification Method For Ladder Diagrams Based On Petri Nets

PLC is an important control device of industrial automation, which is widelyused in some safe-critical systems, including traffic systems, power plants andpetrochemical plants, etc. Thus the reliability and safety of PLC programs arerequired to satisfy strict performances. However, the traditional methods can be usedto identify semanteme and grammar errors, but not logic mistakes in PLC programs.Hence, the verification of PLC programs is broadly studied, and important theoreticresults have been published. Among them, the formal method is the most hopeful.The methods are presented to model ladder diagrams as ordinary Petri nets, andto verify the sequential specifications of ladder diagrams via their Petri-net modelsand NuSMV. They are summarized as follows.1. According to IEC61131-3, algorithms are presented to model some functioninstructions as Petri nets, which are timer, comparison and addition instructions.2. The sequencial specification of ladder diagrams is described by compute treelogic language；3. The sequencial specification is verified with Petri nets models and NuSMV;4. According to the verification results, ladder diagraphs are corrected.Using these methods, the logic mistakes, violating the sequential specification,can be identified automatically. Hence, the reliability and security of ladder programscan be improved. It is hopeful to apply these methods in designing and debuggingof PLC programs.