Medical Device Validation & Verification
Abstract
In this project we adapted a Model Based Design framework to ensure the safety of medical device software and we use implantable pacemaker as case study. The overview of the framework is shown below:
Projects
Incorporating model checking techniques to evaluate both Safety and Efficacy of pacemaker algorithms
The VHM models the Electrophysiology of the heart. It can simulate Electrogram signals for different clinical cases and respond to external pacing signals
An integrated tool chain from model to implementation, which ensures equivalence among models at different level so that key properties are preserved.
Personnel
Resources
Publications
2013 |
|
Jiang, Zhihao; Radhakrishnan, Sriram; Sampath, Varun; Sarode, Shilpa; Mangharam, Rahul 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. @article{VHMCyphy13,
name = {Heart-on-a-Chip: A Closed-loop Testing Platform for Implantable Pacemakers}, author = {Zhihao Jiang and Sriram Radhakrishnan and Varun Sampath and Shilpa Sarode and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/55/}, year = {2013}, date = {2013-04-08}, journal = {Third Workshop on Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy’13)}, } |
2012 |
|
Jiang, Zhihao; Pajic, Miroslav; Moarref, Salar; Alur, Rajeev; Mangharam, Rahul Closed-loop Verification of Medical Devices with Model Abstraction and Refinement (Submitted) (Article) International Journal on Software Tools for Technology Transfer, 2012. @article{STTT12,
name = {Closed-loop Verification of Medical Devices with Model Abstraction and Refinement (Submitted)}, author = {Zhihao Jiang and Miroslav Pajic and Salar Moarref and Rajeev Alur and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/58/}, year = {2012}, date = {2012-09-30}, journal = {International Journal on Software Tools for Technology Transfer}, } |
|
Pajic, Miroslav; Jiang, Zhihao; Lee, Insup; Sokolsky, Oleg; Mangharam, Rahul 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. (BibTeX) @article{TECS13,
name = {Safety-critical Medical Device Development using the UPP2SF Model Translation Tool (Submitted)}, author = {Miroslav Pajic and Zhihao Jiang and Insup Lee and Oleg Sokolsky and Rahul Mangharam}, year = {2012}, date = {2012-09-15}, journal = {ACM TECS RTAS12 Special Issue on Real-Time and Embedded Technology and Applications}, } |
|
Pajic, Miroslav; Jiang, Zhihao; Sokolsky, Oleg; Lee, Insup; Mangharam, Rahul From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study (Article) The 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012), 2012. @article{129,
name = {From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study}, author = {Miroslav Pajic and Zhihao Jiang and Oleg Sokolsky and Insup Lee and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/45/}, year = {2012}, date = {2012-04-04}, journal = {The 18th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2012)}, } |
|
Jiang, Zhihao; Pajic, Miroslav; Moarref, Salar; Alur, Rajeev; Mangharam, Rahul Modeling and Verification of a Dual Chamber Implantable Pacemaker (Article) 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 7214, Page(s): 188-203, 2012. @article{123,
name = {Modeling and Verification of a Dual Chamber Implantable Pacemaker}, author = {Zhihao Jiang and Miroslav Pajic and Salar Moarref and Rajeev Alur and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/43}, year = {2012}, date = {2012-01-06}, journal = {18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)}, volume = {7214}, pages = {188-203}, abstract = {The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the tight coupling of computation, control, and communication. The safety-critical nature and the lack of existing industry standards for verification, make this an ideal domain for exploring applications of formal modeling and analysis. In this study, we use a dual chamber implantable pacemaker as a case study for modeling and verification of control algorithms for medical devices in UPPAAL. We begin with detailed models of the pacemaker, based on the specifications and algorithm descriptions from Boston Scientific. We then define the state space of the closed-loop system based on its heart rate and developed a heart model which can non-deterministically cover the whole state space. For verification, we first specify unsafe regions within the state space and verify the closed-loop system against corresponding safety requirements. As stronger assertions are attempted, the closed-loop unsafe state may result from healthy open-loop heart conditions. Such unsafe transitions are investigated with two clinical cases of Pacemaker Mediated Tachycardia and their corresponding correction algorithms in the pacemaker. Along with emerging tools for code generation from UPPAAL models, this effort enables model-driven design and certification of software for medical devices.}, } The design and implementation of software for medical devices is challenging due to their rapidly increasing functionality and the tight coupling of computation, control, and communication. The safety-critical nature and the lack of existing industry standards for verification, make this an ideal domain for exploring applications of formal modeling and analysis. In this study, we use a dual chamber implantable pacemaker as a case study for modeling and verification of control algorithms for medical devices in UPPAAL. We begin with detailed models of the pacemaker, based on the specifications and algorithm descriptions from Boston Scientific. We then define the state space of the closed-loop system based on its heart rate and developed a heart model which can non-deterministically cover the whole state space. For verification, we first specify unsafe regions within the state space and verify the closed-loop system against corresponding safety requirements. As stronger assertions are attempted, the closed-loop unsafe state may result from healthy open-loop heart conditions. Such unsafe transitions are investigated with two clinical cases of Pacemaker Mediated Tachycardia and their corresponding correction algorithms in the pacemaker. Along with emerging tools for code generation from UPPAAL models, this effort enables model-driven design and certification of software for medical devices.
|
|
Jiang, Zhihao; Pajic, Miroslav; Mangharam, Rahul Cyber-Physical Modeling of Implantable Cardiac Medical Devices (Inproceeding) Proceedings of the IEEE , Page(s): 122 – 137, 2012, ISBN: 0018-9219. @inproceedings{130,
name = {Cyber-Physical Modeling of Implantable Cardiac Medical Devices}, author = {Zhihao Jiang and Miroslav Pajic and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/21/}, isbn = {0018-9219}, year = {2012}, date = {2012-01-03}, booktitle = {Proceedings of the IEEE }, volume = {100}, number = {1}, pages = {122 – 137}, 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.}, } 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.
|
2011 |
|
Jiang, Zhihao; Pajic, Miroslav; Mangharam, Rahul 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 . @article{126,
name = {Model-based Closed-loop Testing of Implantable Pacemakers}, author = {Zhihao Jiang and Miroslav Pajic and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/23/}, isbn = {978-1-61284-640-8 }, year = {2011}, date = {2011-08-18}, journal = {ACM/IEEE 2nd Intl. Conf. on Cyber-Physical Systems (ICCPS’11)}, pages = {131 – 140}, abstract = {The increasing complexity of software in implantable medical devices such as cardiac pacemakers and defibrillators accounts for over 40% of device recalls. Testing remains the principal means of verification in the medical device certification regime. Traditional software test generation techniques, where the tests are generated independently of the operational environment, are not effective as the device must be tested within the context of the patient’s condition and the current state of the heart. It is necessary for the testing system to observe the system state and conditionally generate the next input to advance the purpose of the test. To this effect, a set of general and patient condition-specific temporal requirements is specified for the closed-loop heart and pacemaker system. Based on these requirements, we describe a closed-loop testing environment between a timed automata-based heart model and a pacemaker. This allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate and a trial-ventricle synchrony. We also demonstrate the flexibility and efficacy of the testing environment for more complex common timing anomalies such as reentry circuits, pacemaker mode switch operation and pacemaker-mediated tachycardia. This system is a step toward a testing approach for medical cyber-physical systems with the patient-in-the-loop.}, } The increasing complexity of software in implantable medical devices such as cardiac pacemakers and defibrillators accounts for over 40% of device recalls. Testing remains the principal means of verification in the medical device certification regime. Traditional software test generation techniques, where the tests are generated independently of the operational environment, are not effective as the device must be tested within the context of the patient’s condition and the current state of the heart. It is necessary for the testing system to observe the system state and conditionally generate the next input to advance the purpose of the test. To this effect, a set of general and patient condition-specific temporal requirements is specified for the closed-loop heart and pacemaker system. Based on these requirements, we describe a closed-loop testing environment between a timed automata-based heart model and a pacemaker. This allows for interactive and physiologically relevant model-based test generation for basic pacemaker device operations such as maintaining the heart rate and a trial-ventricle synchrony. We also demonstrate the flexibility and efficacy of the testing environment for more complex common timing anomalies such as reentry circuits, pacemaker mode switch operation and pacemaker-mediated tachycardia. This system is a step toward a testing approach for medical cyber-physical systems with the patient-in-the-loop.
|
|
Jiang, Zhihao; Mangharam, Rahul 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. @inproceedings{235,
name = {Modeling Cardiac Pacemaker Malfunctions with the Virtual Heart Model}, author = {Zhihao Jiang and Rahul Mangharam}, url = {http://repository.upenn.edu/mlab_papers/22/}, year = {2011}, date = {2011-06-20}, booktitle = {33rd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC {textquoteright}11)}, abstract = {Implantable cardiac devices such as artificial pacemakers deliver therapies according to the timing information from the heart. Such devices work under the assumptions of perfect sensing, which are: (a) the pacemaker leads remain in place, and (b) the pacing therapy in one chamber (e.g. atrium) is insulated from the other chambers (e.g. ventricles). But there are common cases which violate these assumptions and the mechanisms for imperfect sensing cannot be captured by a simple signal generator. In this paper we use the Penn Virtual Heart Model (VHM) to investigate the spatial and temporal aspects of the electrical conduction system of the heart in a closed-loop with a pacemaker model. We utilize the spatial properties of the heart to model the sensing mechanism, and use clinical cases to show the validity of our sensing model. Such closed-loop evaluation of the pacemaker operation allows for functional testing of pacemaker software, the development of new algorithms for rhythm therapy and also serves as a tool for incoming cardiac electrophysiology fellows.}, } Implantable cardiac devices such as artificial pacemakers deliver therapies according to the timing information from the heart. Such devices work under the assumptions of perfect sensing, which are: (a) the pacemaker leads remain in place, and (b) the pacing therapy in one chamber (e.g. atrium) is insulated from the other chambers (e.g. ventricles). But there are common cases which violate these assumptions and the mechanisms for imperfect sensing cannot be captured by a simple signal generator. In this paper we use the Penn Virtual Heart Model (VHM) to investigate the spatial and temporal aspects of the electrical conduction system of the heart in a closed-loop with a pacemaker model. We utilize the spatial properties of the heart to model the sensing mechanism, and use clinical cases to show the validity of our sensing model. Such closed-loop evaluation of the pacemaker operation allows for functional testing of pacemaker software, the development of new algorithms for rhythm therapy and also serves as a tool for incoming cardiac electrophysiology fellows.
|
2010 |
|
Jiang, Zhihao; Connolly, Allison; Mangharam, Rahul 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 . @article{125,
name = {Using the Virtual Heart Model to Validate the Mode-Switch Pacemaker Operation}, author = {Zhihao Jiang and Allison Connolly and Rahul Mangharam}, url = {http://repository.upenn.edu/ese_papers/549/}, isbn = {1557-170X }, year = {2010}, date = {2010-08-19}, journal = {32nd Annual International Conference of the IEEE Engineering in Medicine and Biology Society (IEEE EMBC)}, pages = {6690 – 6693 }, abstract = {Artificial pacemakers are one of the most widely-used implantable devices today, with millions implanted worldwide. The main purpose of an artificial pacemaker is to treat bradycardia, or slow heart beats, by pacing the atrium and ventricles at a faster rate. While the basic functionality of the device is fairly simple, there are many documented cases of death and injury due to device malfunctions. The frequency of malfunctions due to firmware problems will only increase as the pacemaker operations become more complex in an attempt to expand the use of the device. One reason these malfunctions arise is that there is currently no methodology for formal validation and verification of medical device software, as there are in the safety-critical domains of avionics and industrial control automation. We have developed a timed-automata based Virtual Heart Model (VHM) to act as platform for medical device software validation and verification. Through a case study involving multiple arrhythmias, this investigation shows how the VHM can be used with closed-loop operation of a pacemaker to validate the necessity and functionality of the complex mode-switch pacemaker operation. We demonstrate the correct pacemaker operation, to switch from one rhythm management mode to another, in patients with supraventricular tachycardias.}, } Artificial pacemakers are one of the most widely-used implantable devices today, with millions implanted worldwide. The main purpose of an artificial pacemaker is to treat bradycardia, or slow heart beats, by pacing the atrium and ventricles at a faster rate. While the basic functionality of the device is fairly simple, there are many documented cases of death and injury due to device malfunctions. The frequency of malfunctions due to firmware problems will only increase as the pacemaker operations become more complex in an attempt to expand the use of the device. One reason these malfunctions arise is that there is currently no methodology for formal validation and verification of medical device software, as there are in the safety-critical domains of avionics and industrial control automation. We have developed a timed-automata based Virtual Heart Model (VHM) to act as platform for medical device software validation and verification. Through a case study involving multiple arrhythmias, this investigation shows how the VHM can be used with closed-loop operation of a pacemaker to validate the necessity and functionality of the complex mode-switch pacemaker operation. We demonstrate the correct pacemaker operation, to switch from one rhythm management mode to another, in patients with supraventricular tachycardias.
|
|
Jiang, Zhihao; Pajic, Miroslav; Connolly, Allison; Dixit, Sanjay; Mangharam, Rahul 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 . @article{124,
name = {Real-time Heart Model for Implantable Cardiac Device Validation and Verification}, author = {Zhihao Jiang and Miroslav Pajic and Allison Connolly and Sanjay Dixit and Rahul Mangharam}, url = {http://repository.upenn.edu/ese_papers/530/}, isbn = {978-1-4244-7546-9 }, year = {2010}, date = {2010-07-16}, journal = {22nd Euromicro Conference on Real-Time Systems, (IEEE ECRTS’10)}, pages = {239 – 248 }, abstract = {Designing bug-free medical device software is challenging, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between 1990 and 2000 affected over 200, 000 devices. This encompasses 41% of the devices recalled and continues to increase in frequency. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to construct a timed-automata model by extracting timing properties of the heart. The platform employs functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has also been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. This integrated functional and formal device design approach has potential to help expedite medical device certification for safe operation.}, } Designing bug-free medical device software is challenging, especially in complex implantable devices that may be used in unanticipated contexts. Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems between 1990 and 2000 affected over 200, 000 devices. This encompasses 41% of the devices recalled and continues to increase in frequency. There is currently no formal methodology or open experimental platform to validate and verify the correct operation of medical device software. To this effect, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning (i.e. during normal sinus rhythm) and malfunctioning (i.e. during arrhythmia) heart. We present a methodology to construct a timed-automata model by extracting timing properties of the heart. The platform employs functional and formal interfaces for validation and verification of implantable cardiac devices. We demonstrate the VHM is capable of generating clinically-relevant response to intrinsic (i.e. premature stimuli) and external (i.e. artificial pacemaker) signals for a variety of common arrhythmias. By connecting the VHM with a pacemaker model, we are able to pace and synchronize the heart during the onset of irregular heart rhythms. The VHM has also been implemented on a hardware platform for closed-loop experimentation with existing and virtual medical devices. This integrated functional and formal device design approach has potential to help expedite medical device certification for safe operation.
|