Model-Based Design of Implantable Cardiac
Devices

Menu:

• Home
• Papers
• Reports
• Videos

Project Overview:

---

Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems affected over 200,000 devices between 1990 and 2000, comprising 41% of the devices recalled. Nonetheless, the only method currently used to check for correctness of the device pperation is unit testing, where a playback of pre-recorded electrogram signals is used to determine if the input signal triggers a particular pacemaker response. This open-loop "tape" testing is unable to check for safety violations due to inappropriate stimulus by the pacemaker, as in the case of Pacemaker Mediated Tachycardia, where the pacemaker drives the heart into an unsafe state. There is, hence, a need for interactive closed-loop verification and testing of such systems.

Pacemaker operation is affected by the refractory and conduction properties of the heart, which are all timing based. Hence, it is natural to model the device and its interaction with the heart using an extension of the timed-automata formalism, which supports powerful verification techniques. We have created a model-driven development framework for safety-critical implantable cardiac devices that includes:
(a) timed-automata based modeling of the controller (i.e., pacemaker) in UPPAAL, model verification, and model-based estimation of the worst-case execution time;
(b) automatic translation of the model to Simulink/Stateflow using the UPP2SF tool;
(c) testing of the translated model; and
(d) automatic modular code synthesis, and testing on a hardware platform.

To enable the framework, we have developed the UPP2SF model-translation tool for automatic translation of verified models (in UPPAAL) to models that may be simulated and tested (in Simulink). The translation guarantees that verified abstract models over-approximate the detailed models used downstream for simulation and code generation, thus ensuring that the closed-loop safety properties are retained through the tool-chain. Finally, for physiologically relevant testing and verification of implantable cardiac devices, we have designed a Virtual Heart Model that: (a) functionally expresses electrophysiological behavior of a healthy and heart during arrhythmia; (b) is formally structured to interface with both modeled and real pacemakers such that the timing of all activity is verifiable by model checking tools; and (c) unlike existing complex, high-order heart models used in (bio)medical research, enables real-time device simulation, and physical testing using the VHM hardware platform.

People:

---

Miroslav Pajic
Zhihao "Hao" Jiang
Prof. Rajeev Alur
Prof. Insup Lee
Prof. Rahul Mangharam
Prof. Oleg Sokolsky

Papers:

---

• Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky, and Rahul Mangharam, "Safety-critical Medical Device Development using the UPP2SF Model Translation Tool", ACM Transactions on Embedded Computing Systems, Accepted.

• Zhihao Jiang, Miroslav Pajic, Rajeev Alur, and Rahul Mangharam, "Closed-loop Verification of Medical Devices with Model Abstraction and Refinement", International Journal on Software Tools for Technology Transfer, 2013. Invited paper.

• Miroslav Pajic, Zhihao Jiang, Insup Lee, Oleg Sokolsky and Rahul Mangharam, "From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study", 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Beijing, China, 2012 (Best Student Paper Award).

• Zhihao Jiang, Miroslav Pajic, Salar Moarref, Rajeev Alur and Rahul Mangharam, "Modeling and Verification of a Dual Chamber Implantable Pacemaker", 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Tallinn, Estonia, 2012 (Best Paper Candidate).

• Zhihao Jiang, Miroslav Pajic and Rahul Mangharam, "Cyber-Physical Modeling of Implantable Cardiac Medical Devices", Proceedings of the IEEE, 2012.

• Zhihao Jiang, Miroslav Pajic and Rahul Mangharam, "Model-based Closed-loop Testing of Implantable Pacemakers", Proc. of the 2nd ACM/IEEE International Conference on Cyber-Physical Systems (ICCPS), Chicago, IL, 2011.

• Zhihao Jiang, Miroslav Pajic, Allison Connolly, Sanjay Dixit and Rahul Mangharam, "Real-time Heart Model for Implantable Cardiac Device Validation and Verification", Proc. of the IEEE Euromicro Conference on Real-Time Systems (ECRTS), Brussels, Belgium, 2010.

Reports:

---

• Miroslav Pajic, Insup Lee, Rahul Mangharam and Oleg Sokolsky, "UPP2SF: Translating UPPAAL Models to Simulink", Technical Report, October 2011.