Formal Modeling Of PLC System With FBD Language And Validation Of The Real-time Property

Programmable logic controller(PLC) is a special device which has sensors and triggers; it can realize the control, simulation and interactive function to the outside. With the widely use of PLC system in various fields, PLC instruction set continues to expand, the complexity of the system also had been greatly improved. As a system with high safety requirements and real-time property, the way to find an efficient modeling and verification method to the system is very necessary.In this paper, through the study I found that there are many shortcomings in the previous methods to ensure the correctness and real-time in PLC system. For example the traditional tests of PLC program dependent on the amount of labor in the debugging process which has not accurate feedback information. The most main is artificial test cannot find all the logic errors, such as race and deadlock. Formal methods are a kind of method based on strict mathematical definition can not only accurate, clear description of system structure and related properties, but also to verify particular properties.Therefore in this paper I analyses the syntax and semantics of FBD programming language, using the formal model oriented approach and put forward a set of relatively complete conversion from FBD language instruction to timed automata steps. After completely modeling of the controller’s programming language instruction, I also abstract modeling PLC system the other three modules, the coordination module, external environment module, loop control module in the timed automata representation. In the model selection I abandon the original model which only care about functional(e.g. system after some operation, eventually reaching some goal state) model(such as Petri or SMV), choosing the timed automata model, add the time factor, especially considering the real-time of the system factor.At the same time, after the completion of modeling every single instruction.I combining with the FBD program control flow and the concept of program logic, puts forward the module combination algorithm and prove the reliability of the algorithm by using UPPAAL tools. Finally, through the example of the conveyor belt, the original system model as timed automata, from the verification result of system, some properties is not passed, indicates some loopholes in original system design. Using the formal method to model the system before the program design can reduce the cost of error and ensure the reliability and robustness of the design.