Once a hazard analysis of a system has been undertaken and a list of safety properties that it must satisfy derived, can this be used to obtain properties which a software controller for the system must satisfy? In addition, what evidential value for the safety of a system are proofs of correctness of a formal specification of its software components? We will examine these issues in the context of a specification and development technique for the B formal specification language, which has been used to specify and design discrete event control systems for batch-processing plants. A simple example is used to illustrate the ideas. The results obtained from a larger case study are also presented.