Design Method For PLC Program Based On Timed Automata Theory And Its Application

With the increasing complexity of industrial control systems,the functional requirements are also increasing and the number of states is huge,and PLC needs to complete more and more complex control tasks on site as much as possible.In addition,there are higher safety requirements for intelligent CNC systems in applications such as unattended workshops and smart factories.Traditional PLC program design methods can't guarantee the correctness and safety of the complex control system.Designing programs using traditional PLC program methods leads to tedious programming and testing,and PLC software platforms can only detect grammatical errors,but they can't detect logic errors,and manual tests cannot guarantee that all logic errors are found.In view of the above inadequacies,this paper proposes a design method for PLC program based on timed automata theory.Based on the analysis of the time automata theory and the grammar definition of sequence function chart programming language defined in IEC61131-3 standard,the detailed and complete transformation rules from UPPAAL time automaton models to PLC programs written in the languages of IEC61131-3 standard are designed,including the transformation of locations and transfer edges,the transformation of synchronization channels and the transformation of variable declarations and the system declarations.According to transformation rules,the specific algorithm of transforming UPPAAL time automata models into PLC programs is designed.And the model conversion tool TA2 PLC which can automatically generate PLC programs written in the languages of IEC61131-3standard,is designed using Python programming language.On the basis of the above work,the overall flow of the design method for PLC program based on timed automata theory is given.And the PLC program design of a four story elevator control system is used as an experiment.The formal model is established and correctness and safety properties of the system are verified based on timed automata theory in UPPAAL.The complete PLC programs of the elevator control system written in the languages of IEC61131-3 standard is automatically generated by the TA2 PLC tool.The application of this method to safety control functions for iNC is introduced.In the design method for PLC program based on timed automata theory,the logicbetween the states of subsystems is clear and intuitive,which can simplify the programming difficulty of the complex system application logic,and the formal simulations and verifications can ensure the correctness and safety properties of PLC program application logic.The function blocks written in sequence function chart programming language in the PLC program automatically generated by TA2 PLC have a great program structure to facilitate the subsequent debugging and maintenance.