In　order　to　ensure　the　safety　of　equipment　and　persons,　the　rigorous　requirements　on　the　correctness　and　reliability　of　control　program　are　always　needed　in　industrial　control　system.　The　traditional　program　design　methods　are　based　on　the　realization　of　the　functions　and　verified　by　the　simulations　and　tests.　Errors　can　only　be　founded　during　the　simulation　and　test　phase.　And　some　vital　errors　cannot　be　tested,　because　these　errors　may　cause　damages　to　the　equipment　and　persons.　So　the　correctness　and　reliability　of　control　program　cannot　be　ensured.　For　these　problems,　the　formal　design　methods　emerged　as　the　times　require.　The　errors　can　be　found　in　design　level　by　the　formalized-model.　In　other　word,　formal　methods　could　detect　the　errors　earlier,　reduce　the　cost　of　development,　and　are　suitable　for　the　occasions　that　require　rigorous　requirements　on　the　correctness　and　reliability.　This　paper　discussed　a　kind　of　Event-B　based　formal　method,　using　Rodin　Platform,　to　model,　refine　and　verify　the　automated　production　line　control　system.