Abstract: Formal methods are very efficient techniques for formal verification of a specification and to find errors in early stage of the system development. In order to generate a high quality code from a formal specification particularly in the embedded system is highly indispensable and a de-facto standard in many industrial application domains, such as medical, avionics and automotive control. This paper presents automatic source code generation from the developed formal specifications of a cardiac pacemaker. Cardiac pacing system is a Grand Challenge in the area of Software Verification. This paper includes an architecture of automatic code generation tool, summary of a formal development of the cardiac pacemaker using refinement techniques in Event-B, code generation of the developed formal model into C, C++, Java and C\# using code generation tool EB2ALL, and finally the code compilation and execution.