Modeling and Verification of Intelligent Manufacturing Product Line System with Timed Automata

At present, intelligent manufacturing such as intelligent equipment and intelligent factory is leading the transformation of manufacturing mode, and the deep integration of the new generation of information technology and manufacturing industry has reached a new stage. However, intelligent production system has the characteristics of high real-time and unpredictability. Therefore, it is necessary to refine the design model according to the specifications of intelligent production system to ensure the correctness, availability and liveness of the system and avoid defects in the design stage. Aiming at the limitation of traditional methods, a modeling and analysis method of intelligent production line using formal method is proposed. Taking the automatic welding product line system as an example, CTL(Computation Tree Logic) formal language is used to describe the system requirement specification, and the time automata model of the components in each stage of the production line is constructed in UPPAAL. Finally, real-time verification and correctness verification are carried out for the whole system to ensure that the system can meet the requirement specirication. The experimental results show that the system can make self-decision and then recovery when encountering unexpected faults, and the accuracy of the system is guaranteed, which provides effective guidance and reference for system design.