A Model Driven Approach for Cardiac Pacemaker Design Using a PRET Processor

Implantable medical devices such as cardiac pacemakers have been recalled frequently with safety related issues. This paper proposes a model driven approach for pacemaker design by combining the strengths of two well-known philosophies for safety critical systems. First, we adopt the SCCharts synchronous language for pacemaker specification. Second, we adopt a PRET architecture for the underlying processor which has been modified to include reactive semantics. PRET processors offer an ideal platform for providing timing guarantees. We use automatic code generation combined with static timing analysis during the design phase. Also, we use an existing emulation model of the human heart using a 33-node conduction network for closed loop validation of the designed pacemaker.