Research On PLC Program Design And Formal Mathod Of 125I Automated Production Line

Automated production line is a kind of automatic control system in modern production progress, with high efficiency, good progress quality and low production cost. An automated production line is usually composed of mechanical and electrical equipment with high level of integration and automation to include all aspect of the production progress and reduce manual operations. These features ask for high reliability. To verify the correctness of program, a large number of time and tests for detecting errors are needed before the production line actually working. However, some sort of errors may not be detected by testing due to lack of testing methods or time. And some vital errors cannot be tested in critical system, even though they have been designed the exception handlers, because these errors may cause damages to the equipment and persons. For these problems, the formal methods emerged as the times require. Formal methods are based on mathematics, can identify these errors and verify the correctness of exception handlers at the modeling stage by modeling and verifying the actual system, instead of testing. So, formal methods can reduce the cost of development, and are suitable for the occasions that required rigorous requirements on correctness and reliability.This paper researches on the design and reliability verification of 125 I automated production line, including PLC system design methods and relative technology. Because of the rigorous requirements on correctness and reliability of 125 I automated production line, there tried the Event-B formal method except for simulation and test. Meanwhile, this paper introduces the related theorem of formal methods and the Event-B modeling and verification method.