To overcome the defects in traditional PLC programming, an approach combined formal methods with Signal Interpreted Petri Net (SIPN) is presented. An example of robot welding unit is used to illustrate this process. This paper builds a model of the control algorithm with Signal Interpreted Petri Net first, and verifies whether it satisfies the safety, liveness and reversibility characteristics of basic Petri net. Then it uses the model checking tool Cadence SMV for model verification and validation, to test whether it meets the properties of certainty, termination and output correctness. Thus the possible events like concurrency, conflict and deadlock in control algorithm designing process can be avoided and correct and dependable PLC programs are designed.