Close Loop Verification of Implantable Cardiac Devices
The main project objective is to develop a framework for the formal verification of ICD control software. Several goals have been outlined to meet this objective: (1) identify clinical data sets that provide adjudicated signals (i.e. identification of arrhythmia onset and classification by a physician) and that are compatible with the ICD control software; (2) develop numerical simulations that provide a method of generating self-adjudicated signals compatible with the ICD control software; (3) develop an ICD control-software model based on key temporal and frequency signal properties to perform arrhythmia detection and classification (e.g. VT/supra vs. VT/VF in the ventricle); and (4) apply verification techniques to the ICD model such as open-loop sensitivity analysis and closed-loop specificity analysis that will quantitatively assess rates of inappropriate ICD shocking...
Our verification framework will be based on a high-fidelity model that captures the heart’s electrophysiological behavior under the ICD’s control at an appropriate level of detail. We are exploring three formalisms to identify the model: i) Differential Equations-based Models, ii) Hybrid Automata (HA) and iii) Timed Automata (TA). DEMs forms the basis of modeling the heart’s electrophysiology, which is characterized by the emergent patterns of electrical energy observed at the tissue (macro)-level. HA are ideally suited for capturing interactions between analog physical processes, such as cardiac excitation, and digital control systems, such as the ICD. HA can also be used to approximate the highly nonlinear cell-level behaviors for tractable verification. TA, a subclass of HA, have been successfully used for pacemaker verification by an UPenn team and represent a powerful modeling formalism for cardiac cells.
Compositionality and Approximate Abstraction
Verification of ICDs often runs into the well known State Explosion problem. Given a property of interest the choice of the cardiac model with the requisite level of detail is critical for formal verification. Two technologies that will be developed to facilitate the choice of the model, and then tractable verification are i) compositionality and ii) approximate abstraction. Compositionality enables us to reason about a complex system in terms of its components, also known as subsystems. In our case, the electrophyisiological behavior of the heart under the influence of the ICD will be modeled using two subsystems: a cardiac DEM H and a computational model D of the ICD. The composed model, denoted by H × D, will capture the electrical behaviors of the heart induced by the ICD’s control algorithms. Approximate abstraction, on the other hand, refers to the process of identifying an approximate abstract models H' and D' corresponding to a detailed model H and D, respectively, which removes the complexity of a model while preserving the properties that are relevant to verification.
Time Frequency Logic (TFL) Specification
A major safety requirement of ICDs is that Ventricular Tachycardia (VT) must be detected and appropriate therapeutic shocks must be delivered to restore the sinus rhythm of the heart. VT, which is primarily characterized by an increase in the heart rate, is diagnosed on the basis of electrogram signals sensed by the leads of the ICD. In this regard, a major safety concern with ICDs is inappropriate shocking, which is defined as the delivery of inappropriate or unnecessary doses of electrical shocks either due to sensing errors, or misdetection of VT on the basis of electrograms. The ICD software is prone to incorrectly detect SVT as VT leading to inappropriate shocking. SVT, such as AFib, originate in the upper chambers of the heart and ICD shocks must be ideally withheld in such cases. Since electrograms form the basis of VT-SVT discrimination, and the overall operation of the ICDs, requirements will be learned and specified using temporal and frequency-domain aspects of electrograms. Following are some of the features of electrograms that will be used to specify the requirements: heart rate, variability in cycle lengths, QRS complex morphology, atrio-ventricular heart rate ratio, dominant frequency, and sudden onset criteria.
 Md. Ariful Islam, Rance Cleaveland, Flavio H. Fenton, Radu Grosu, Paul L. Jones, Scott A. Smolka. Probabilistic Reachability for Multi-Parameter Bifurcation Analysis of Cardiac Alternans. Theoretical Computer Science (TCS), 2018.
 Md. Ariful Islam, Hyunkung Lim, Nicola Paoletti, Houssam Abbas, Zhihao Jiang, Jacek Cyranka, Rance Cleaveland, Sicun Gao, Edmund Clarke, Radu Grosu, Rahul Mangharam, Elizabeth Cherry, Flavio Fenton, Richard A. Gray, James Glimm, Shan Lin, Qinsi Wang, and Scott A. Smolka: CyberCardia Project: Modeling, Verification and Validation of Implantable Cardiac Devices. IEEE International Conference on Bioinformatics and Biomedicine (BIBM), 2016.
 A. Murthy, Md. A. Islam, S. A. Smolka, and R. Grosu (2016). Computing Compositional Proofs of Input-to-Output Stability Using SOS Optimization and delta-Decidability. Nonlinear Analysis: Hybrid Systems.
 Md. A. Islam, G. Byrne, S. Kong, E. M. Clarke, R Cleaveland, F. H. Fenton, R. Grosu, S. A. Smolka (2016). Bifurcation Analysis of Cardiac Alternans using delta-Decidability. Proceedings of CMSB 2016, The 14th Conference on Computational Methods in Systems Biology.
 Md. A. Islam, Q. Wang, E. M. Clarke, S. A. Smolka, R. Hsani, Radu Grosu, O. Balun (2016). Probabilistic Reachability Analysis of the Tap Withdrawal Circuit in Caenorhabditis elegans. Proceedings of HLDVT 2016: The 18th IEEE International High-Level Design Validation and Test Workshop.