Research On The Method For Modeling And Analyzing PLC Programs Based On Petri Nets

Programmable logic controllers (PLCs) are significant control devices forautomation in modern discrete processing enterprises. They have been widely used insafe-critical systems, such as railway, nuclear power stations, petrochemical plantsand defense industry. Therefore, it is great important to guarantee the safety andreliability of PLC programs. For the PLC, the correctness of programs is hard to beassured with respect to the reliability of hardware. The conventional development ofPLC programs is that the programs are designed according to the control objectionsand then confirmed by reduplicate debugging. Therefore, the workload is great heavyand the reliability of programs is difficult to be guaranteed. Moreover, along with theincreasing amount of sensors and actuators in the system, the state space is toexplode; this makes it difficult or even impossible to locate all logical mistakes in aladder diagram (LD) program by debugging and detecting item by item. As a result,the cost and cycle of development will rise, and even the human safety will bemenaced.The formal methods fulfill the maintenance and rectification of system fromformal designation and formal verification. The formal designation models a systemby using formal language, improves the model after analyzing its properties based onthe specification what the system should fulfill; this can avoid exhausted testing in theconventional development. The formal verification not only changes the situation thatthe system behaviors which are verified in the conventional testing are limited, butalso improves the efficiency of detection of logic mistakes. Hence, the formal methodis the indispensable way by complementing the conventional testing method.Petri nets (PNs) are emerging as a very promising formal tool to validate andverify LD programs, which are intuitive and have precise mathematic foundation,since they are well applicable to model and analyze PLC systems. In this paper, weintroduce the method which is to translate LDs to PNs and the methods for analyzingand detecting the race of LDs based on the PN models: (1) According to IEC61131-3, an LD is abstracted as a kind of data structurebased on its semantics, and then the corresponding PN model is translatedfrom this data structure.(2) According to the working principle of PLC, the state space of PLC system iscomputed based on the reachable graph of its PN model.(3) Using the state space of a PLC system, the instructions which incur the racecan be detected and located.This paper presents a systematic and comprehensive translating algorithm froman LD program to an ordinary PN, the method for computing the state space of PLCsystem based on reachability graph of PN model and detecting the race in programs.It is possible to simulate the dynamic behavior of LD programs and efficientlyanalyze the properties of programs using the PN theory that is well developed forordinary PNs. The race detection can avoid the loss caused by the race condition andmake an effort to the formal verification of PLC programs.