Before　the　automatic　production　line　put　into　practical　use　in　industrial　domain,　it　must　go　through　a　large　number　of　long-term　rigorous　test　to　detect　errors　in　the　design　process.　However　in　the　actual　test　process,　the　same　mistake　leads　to　different　results　due　to　the　different　test　methods　and　there　are　some　special　conditions　resulting　from　the　limitation　of　field　test　environment　what　can＇t　be　used　to　be　tested.　The　formal　method,　by　using　the　method　of　discrete　mathematics　to　practical　system　mathematical　modeling　and　validation,　can　replace　the　methods　what　can　not　been　tested　under　the　conditions　of　system　verification.　The　formal　method　is　also　suitable　for　developing　large　reactive　and　distributed　systems.　In　this　paper,　the　specific　formal　method　which　is　called　Event-B　improves　the　high　security　and　reliability　of　system.　Moreover　the　related　tools　such　as　Rodin　are　used　for　modeling,　refinement　and　verification　in　the　PLC　(Programmable　Logic　Controller)　automatic　production　line.　The　result　in　this　paper　shows　that　our　approach　contributes　to　reducing　system　details　during　the　early　development　stage　and　leads　to　simpler　proofs　and　more　automated　proofs.　Thus　it　provides　a　new　method　for　reference　for　higher　requirements　in　the　reliability　in　engineering　projects,　so　as　to　ensure　the　correctness　of　the　designed　software.