Penn Virtual Heart Model (VHM)
Abstract
The design of bug-free and safe medical device software is challenging, especially in complex implantable devices that control and actuate organs in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators between 1990 and 2000 affected over 600,000 devices. Of these, 200,000 or 41%, were due to firmware issues and their effect continues to increase in frequency. There is currently no formal methodology or open experimental platform to test and verify the correct operation of medical device software within the closed-loop context of the patient. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning and malfunctioning (i.e., during arrhythmia) heart. By extracting the timing properties of the heart and pacemaker device, we present a methodology to construct a timed-automata model for functional and formal testing and verification of the closed-loop system. The VHM’s capability of generating clinically-relevant response has been validated for a variety of common arrhythmias. Based on a set of requirements, we describe a closed-loop testing environment that allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate, atrial-ventricle synchrony and complex conditions such as pacemaker-mediated tachycardia. This system is a step toward a testing and verification approach for medical cyber-physical systems with the patient-in-the-loop.
Let our heart catch the bugs before your heart does.
Personnel
Publications
2013 |
|
Heart-on-a-Chip: A Closed-loop Testing Platform for Implantable Pacemakers (Article) Third Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy’13), 2013. |
2012 |
|
Closed-loop Verification of Medical Devices with Model Abstraction and Refinement (Submitted) (Article) International Journal on Software Tools for Technology Transfer, 2012. |
|
Safety-critical Medical Device Development using the UPP2SF Model Translation Tool (Submitted) (Article) ACM TECS RTAS12 Special Issue on Real-Time and Embedded Technology and Applications, 2012. |
|
Cyber-Physical Modeling of Implantable Cardiac Medical Devices (Inproceeding) Proceedings of the IEEE , Page(s): 122 – 137, 2012, ISBN: 0018-9219. |
2011 |
|
Model-based Closed-loop Testing of Implantable Pacemakers (Article) ACM/IEEE 2nd Intl. Conf. on Cyber-Physical Systems (ICCPS’11), Page(s): 131 – 140, 2011, ISBN: 978-1-61284-640-8 . |
|
Modeling Cardiac Pacemaker Malfunctions with the Virtual Heart Model (Inproceeding) 33rd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC {textquoteright}11), 2011. |
2010 |
|
Using the Virtual Heart Model to Validate the Mode-Switch Pacemaker Operation (Article) 32nd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (IEEE EMBC), Page(s): 6690 – 6693 , 2010, ISBN: 1557-170X . |
|
Real-time Heart Model for Implantable Cardiac Device Validation and Verification (Article) 22nd Euromicro Conference on Real-Time Systems, (IEEE ECRTS’10), Page(s): 239 – 248 , 2010, ISBN: 978-1-4244-7546-9 . |