The Control Program Design And Formal Mathod Validation Of ¹²⁵I Automatic Production Line

The automatic production line due to its high efficiency, stable processing, and many other advantages has been widely applied to various control field. The automation technology not only can make people from heavy manual labor, parts of mental Labour and bad, dangerous work environment, greatly improve the labor productivity. In recent years, radioactive iodine(¹²⁵I) medical product seal seed source has good effect in the treatment of malignant tumor, and use the automated production line production can greatly improve the efficiency of production, at the same time can avoid the effect of unstable factors of production. Before automatic production line put into the industrial sector, it must go through a lot of rigorous testing for a long time, so as to detect errors in the design process. However seed source iodine(¹²⁵I)seal because this topic based on 125 I automatic production line project, the paper with iodine(¹²⁵I) the design of the automatic production line control program and formal method validation as the research object, the main research work and research results were as follows:First of all, the design of the 125 I automatic production line control structure is completed. Automatic production lines, a detailed analysis on the one hand, in 125 I demand, on the basis of according to the actual production process, the loading process of mechanical structure design and installation, welding and tumble, and sensor to replace the timer judging location positioning. According to the progress of the project, field added some control equipment, including embedded server, touch screen, laser welding machine and so on, using the SIMATIC MANAGER has formed a completed network system, can realize data sharing between equipment, the production data backup, remote control and monitoring and so on.Second, the design of the 125 I automatic production line control program is completed. Under the premise of considering production line may appear a variety of fault, on the one hand, through using the HIGRAPH state diagram method to design software programming for main transmission functions of the production line and 5 location, which can conveniently realize the fault screen processing, at the same time for some abnormalities in writing to its corresponding test procedure for processing, use of type structure of a program status table to realize variable change management. Through the production line of OPC technology to achieve the data transfer between different devices, solve the problem of the heterogeneous between the communication equipment, according to the requirements development projects at the same time OPC client implementation customization of production data storage.Finally, the EVENT-B formal methods proposed to do mathematical modeling and validation for the 125 I automatic production line control program. On the detailedanalysis of the EVENT-B based on the principle of formal methods, in strict accordance with the EVENT-B language specification description of system security and functional requirements, formulate the accurate detailed elaboration strategy, and through the vertical and horizontal refinement gradually introduce new element function of new design system model was constructed to prove relevant Proof Obligation, so as to ensure the safety of the design model and the accuracy.