@booklet {, title = {Neural Simplex Architecture}, year = {2020}, author = {Dung T. Phan and Radu Grosu and Nils Jansen and Nicola Paoletti and Scott A. Smolka and Scott D. Stoller} } @conference {, title = {Towards Automated Comprehension and Alignment of Cardiac Models at the System Invariant Level}, booktitle = {CSBio{\textquoteright}20: Proceedings of the Eleventh International Conference on Computational Systems-Biology and Bioinformatics}, year = {2020}, author = {Huang, Samuel and Diep, Madeline and Jang, Kuk and Cherry, Elizabeth M and Fenton, Flavio H and Cleaveland, Rance and Lindvall, Mikael and Mangharam, Rahul and Porter, Adam} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, volume = {765}, year = {2019}, pages = {158{\textendash}169}, author = {Islam, Md Ariful and Cleaveland, Rance and Fenton, Flavio H and Grosu, Radu and Jones, Paul L and Smolka, Scott A} } @article {, title = {An Algebraic Framework for Runtime Verification}, journal = {CoRR}, volume = {abs/1802.03775}, year = {2018}, url = {http://arxiv.org/abs/1802.03775}, author = {Stefan Jaksic and Ezio Bartocci and Radu Grosu and Dejan Nickovic} } @article {, title = {Probabilistic reachability for multi-parameter bifurcation analysis of cardiac alternans}, journal = {Theoretical Computer Science}, year = {2018}, month = {02/2018}, abstract = {

Using a probabilistic reachability-based approach, we present a multi-parameter bifurcation analysis of electrical alternans in the two-current Mitchell{\textendash}Schaeffer (MS) cardiac-cell model. Electrical alternans is a phenomenon characterized by a variation in successive Action Potential Durations generated by a cardiac cell or tissue. Alternans are known to initiate re-entrant waves and are an important physiological indicator of an impending life-threatening arrhythmia such as ventricular fibrillation. The multi-parameter bifurcation analysis we perform identifies a bifurcation hypersurface in the MS model parameter space, such that a small perturbation to this region results in a transition from highly likely alternans to highly likely non-alternans behavior. Our approach to this problem rests on encoding alternans-like behavior in the MS model as a five-mode, multinomial hybrid automaton. To perform multi-parameter bifurcation analysis of cardiac alternans, we first treat the parameters in question as bounded random variables. We then apply a sophisticated guided-search-based probabilistic reachability analysis to compute a bounded bifurcation region (possibly very tight) that contains the bifurcation hypersurface (BH). Our probabilistic reachability analysis uses a technique that combines a δ-decision procedure with statistical tests. In the process of computing the bifurcation region, we further partition the parameter space into two more regions such that any valuation chosen from one of the regions will either produce alternans or non-alternans behavior with a probability greater than a user-defined threshold.

}, keywords = {Bifurcation analysis, Cardiac alternans, Cardiac modeling, Formal methods, Hybrid systems, Probabilistic reachability}, issn = {0304-3975}, doi = {https://doi.org/10.1016/j.tcs.2018.02.005}, url = {http://www.sciencedirect.com/science/article/pii/S0304397518300823}, author = {Md. Ariful Islam and Rance Cleaveland and FLAVIO H. FENTON and Radu Grosu and Paul L. Jones and Scott A. Smolka} } @conference {, title = {Lagrangian Reachabililty}, booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017 Proceedings, Part {I}}, year = {2017}, abstract = {

We introduce LRT, a new Lagrangian-based ReachTube computation algorithm that conservatively approximates the set of reachable states of a nonlinear dynamical system. LRT makes use of the Cauchy-Green stretching factor (SF), which is derived from an over-approximation of the gradient of the solution flows. The SF measures the discrepancy between two states propagated by the system solution from two initial states lying in a well-defined region, thereby allowing LRT to compute a reachtube with a ball-overestimate in a metric where the computed enclosure is as tight as possible. To evaluate its performance, we implemented a prototype of LRT in C++/Matlab, and ran it on a set of well-established benchmarks. Our results show that LRT compares very favorably with respect to the CAPD and Flow* tools.

}, doi = {10.1007/978-3-319-63387-9_19}, author = {Jacek Cyranka and Md. Ariful Islam and Greg Byrne and Paul L. Jones and Scott A. Smolka and Radu Grosu} } @conference {, title = {A novel ICD morphology discriminator to improve discrimination between Ventricular and Supraventricular tachycardias}, booktitle = {In Heart Rhythm Scientific Sessions, Chicago}, year = {2017}, month = {05/2017}, abstract = {

Implantable\ \  \ Cardioverter\ \  \ Defibrillator\ \  \ (ICD)\ \  \ morphology\ \  \ discriminators\ \  \ (MDs)\ \  \ discriminate\ \  \ ventricular\ \  \ (VT)\ \  \ from\ \  \ supraventricular\ \  \ tachycardias\ \  \ (SVT)\ \  \ by\ \  \ comparing\ \  \ single-beat\ \  \ electrogram\ \  \ (EGM)\ \  \ shape\ \  \ during\ \  \ tachycardia\ \  \ versus\ \  \ sinus\ \  \ rhythm\ \  \ (Fig.\ \  \ A)\ \  \ and\ \  \ counting\ \  \ the\ \  \ matches.\ \  \ \ \  \ 
Objective

}, author = {H. Abbas and K.J. Jang and J. Liang and S. Dixit and R. Mangharam} } @article {, title = {Simultaneous Quantification of Spatially Discordant Alternans in Voltage and Intracellular Calcium in Langendorff-Perfused Rabbit Hearts and Inconsistencies with Models of Cardiac Action Potentials and Ca Transients}, journal = {Frontiers in Physiology}, volume = {8}, year = {2017}, doi = {10.3389/fphys.2017.00819}, url = {https://doi.org/10.3389/fphys.2017.00819}, author = {Ilija Uzelac and Yanyan C. Ji and Daniel Hornung and Johannes Schr{\"o}der-Scheteling and Stefan Luther and Richard A. Gray and ELIZABETH M. CHERRY and FLAVIO H. FENTON} } @conference {, title = {Automated Closed-Loop Model Checking of Implantable Pacemakers using Abstraction Trees}, booktitle = {Medical Cyber Physical Systems Workshop 2016}, year = {2016}, abstract = {

Autonomous medical devices such as implantable cardiac pacemakers are capable of diagnosing the patient condition and delivering therapy without human intervention. Their ability to autonomously affect the physiological state of the patient makes them safety-critical. Sufficient evidence for the safety and efficacy of the device software, which makes these autonomous decisions, should be provided before these devices can be released on the market. Formal methods like model checking can provide safety evidence that the devices can safely operate under a large variety of physiological conditions. The challenge is to develop physiological models that are general enough to cover the large variability of human physiology, and also expressive enough to provide physiological contexts to counter-examples returned by the model checker. In this paper, the authors develop a set of physiological abstraction rules that introduce physiological constraints to heart models. By applying these abstraction rules to a initial set of heart models, an abstraction tree is created. The root model covers all possible inputs to a pacemaker and derived models cover inputs from different heart conditions. If a counter-example is returned by the model checker, the abstraction tree is traversed so that the most concrete counter-example(s) with physiological contexts can be returned to the domain experts for validity check. The abstraction tree framework replaces the manual abstraction and refinement framework, which reduced the amount of domain knowledge required to perform closed-loop model checking. It encourages the use of model checking during the development of autonomous medical devices, and identifies safety risks earlier in the design process.

}, author = {Zhihao Jiang and Houssam Abbas and Pieter J Mosterman and Rahul Mangharam} } @conference {, title = {Bifurcation Analysis of Cardiac Alternans Using δ -Decidability.}, booktitle = {CMSB}, year = {2016}, publisher = {Springer}, organization = {Springer}, keywords = {dblp}, isbn = {978-3-319-45176-3}, url = {http://dblp.uni-trier.de/db/conf/cmsb/cmsb2016.html$\#$IslamBKCCFGJS16}, author = {Islam, Md. Ariful and Byrne, Greg and Kong, Soonho and Clarke, Edmund M. and Cleaveland, Rance and Fenton, Flavio H. and Grosu, Radu and Jones, Paul L. and Smolka, Scott A.}, editor = {Bartocci, Ezio and Li{\`o}, Pietro and Paoletti, Nicola} } @article {, title = {The Challenges of High-Confidence Medical Device Software}, journal = {IEEE Computer January Outlook}, year = {2016}, author = {Z. Jiang and H. Abbas and K. Jang and R. Mangharam} } @conference {, title = {Cybercardia project: Modeling, verification and validation of implantable cardiac devices}, booktitle = {2016 IEEE International Conference on Bioinformatics and Biomedicine (BIBM)}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, author = {Islam, Md Ariful and Lim, Hyunkyung and Paoletti, Nicola and Abbas, Houssam and Jiang, Zhihao and Cyranka, Jacek and Cleaveland, Rance and Gao, Sicun and Clarke, Edmund and Grosu, Radu and others} } @conference {, title = {High-level modeling for computer-aided clinical trials of medical devices}, booktitle = {High Level Design Validation and Test Workshop (HLDVT), 2016 IEEE International}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, abstract = {

Medical devices like the Implantable Cardioverter Defibrillator (ICD) are life-critical systems. Malfunctions of the device can cause serious injury or death of the patient. In addition to rigorous testing and verification during the development process, new medical devices often go through clinical trials to evaluate their safety and performance on sample populations. Clinical trials are costly and prone to failure if not planned and executed properly. Evaluating devices on computer models of the relevant physiological systems can provide helpful insights into the safety and efficacy of the device, thus helping to plan and execute a clinical trial. In this paper, we demonstrate how to develop high-level physiological models of cardiac electrophysiology and how to apply them to the Rhythm ID Head to Head Trial (RIGHT), a 5-year long clinical trial for comparing two ICDs. We refer to this as a Computer-Aided Clinical Trial (CACT). We explored two modeling options, a white-box model capturing the mechanisms of the physiological behaviors, and a blackbox model which uses machine learning methods to synthesize physiological input signals. Both models were able to generate physiological inputs to the ICDs and we discuss the challenges and appropriateness of the two modeling options.

}, author = {Abbas, Houssam and Jiang, Zhihao and Jang, Kuk Jin and Beccani, Marco and Liangy, Jackson and Mangharam, Rahul} } @conference {, title = {In-silico pre-clinical trials for implantable cardioverter defibrillators}, booktitle = {Engineering in Medicine and Biology Society (EMBC), 2016 IEEE 38th Annual International Conference of the}, year = {2016}, publisher = {IEEE}, organization = {IEEE}, abstract = {

Regulatory authorities require that the safety and efficacy of a new high-risk medical device be proven in a Clinical Trial (CT), in which the effects of the device on a group of patients are compared to the effects of the current standard of care. Phase III trials can run for several years, cost millions of dollars, and expose patients to an unproven device. In this paper, we demonstrate how to use a large group of synthetic patients based on computer modeling to improve the planning of a CT so as to increase the chances of a successful trial for implantable cardioverter defibrillators (ICDs). We developed a computer model of the electrical generation and propagation in the heart. This model was used to generate a large group of heart instances capable of producing episodes of 19 different arrhythmias. We also implemented two arrhythmia detection algorithms from the literature: Rhythm ID from Boston Scientific and PR Logic + Wavelet from Medtronic. Using this setup, we conducted multiple in-silico trials to compare the ability of the two algorithms to appropriately discriminate between potentially fatal Ventricular Tachy-arrhythmias (VT) and nonfatal Supra-Ventricular Tachy-arrhythmias (SVTs). The results of our in-silico trial indicate that Rhythm ID was less able to discriminate between SVT and VT and so may lead to more cases of inappropriate therapy. This corroborates the findings of the Rhythm ID Going Head to Head Trial (RIGHT), a clinical trial that compared the two algorithms in patients. We further demonstrated that the result continues to hold if we vary the distribution of arrhythmias in the synthetic population. We also used the same in-silico cohort to explore the sensitivity of the outcome to different parameter settings of the device algorithms, which is not feasible in a real clinical trial. In-silico trials can provide early insight into the factors which affect the outcome of a CT at a fraction of the cost and duration and without the ethical issues.

}, author = {Jiang, Zhihao and Abbas, Houssam and Jang, Kuk Jin and Beccani, Marco and Liang, Jackson and Dixit, Sanjay and Mangharam, Rahul} } @conference {, title = {Towards Model Checking of Implantable Cardioverter Defibrillators}, booktitle = {Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control}, year = {2016}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, abstract = {

Ventricular Fibrillation is a disorganized electrical excitation of the heart that results in inadequate blood flow to the body. It usually ends in death within a minute. A common way to treat the symptoms of fibrillation is to implant a medical device, known as an Implantable Cardioverter Defibrillator (ICD), in the patient{\textquoteright}s body. Model-based verification can supply rigorous proofs of safety and efficacy. In this paper, we build a hybrid system model of the human heart+ICD closed loop, and show it to be a STORMED system, a class of o-minimal hybrid systems that admit finite bisimulations. In general, it may not be possible to compute the bisimulation. We show that approximate reachability can yield a finite simulation for STORMED systems, and that certain compositions respect the STORMED property. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.

}, keywords = {heart modeling, icds, life-critical cps, medical devices, stormed systems}, isbn = {978-1-4503-3955-1}, doi = {10.1145/2883817.2883841}, url = {http://doi.acm.org/10.1145/2883817.2883841}, author = {Abbas, Houssam and Jiang, Kuk Jin and Jiang, Zhihao and Mangharam, Rahul} } @article {, title = {High-Confidence Medical Device Software Development}, journal = {Foundations and Trends in Electronic Design Automation}, volume = {9}, year = {2015}, abstract = {

The design of bug-free and safe medical device software is challenging, especially in complex implantable devices. This is due to the device{\textquoteright}s closed-loop interaction with the patient{\textquoteright}s organs, which are stochastic physical environments. The life-critical nature and the lack of existing industry standards to enforce software validation make this an ideal domain for exploring design automation challenges for integrated functional and formal modeling with closed-loop analysis. The primary goal of high-confidence medical device software is to guarantee the device will never drive the patient into an unsafe condition even though we do not have complete understanding of the physiological plant. There are two major differences between modeling physiology and modeling man-made systems: first, physiology is much more complex and less well-understood than man-made systems like cars and airplanes, and spans several scales from the molecular to the entire human body. Secondly, the variability between humans is orders of magnitude larger than that between two cars coming off the assembly line. Using the implantable cardiac pacemaker as an example of closed-loop device, and the heart as the organ to be modeled, we present several of the challenges and early results in model-based device validation. We begin with detailed timed automata model of the pacemaker, based on the specifications and algorithm descriptions from Boston Scientific. For closed-loop evaluation, a real-time Virtual Heart Model (VHM) has been developed to model the electrophysiological operation of the functioning and malfunctioning (i.e., during arrhythmia) hearts. By extracting the timing properties of the heart and pacemaker device, we present a methodology to construct timed-automata models for formal model checking and functional testing of the closed-loop system. The VHM{\textquoteright}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 framework of Abstraction Trees that allows for interactive and physiologically relevant closed-loop model checking and testing for basic pacemaker device operations such as maintaining the heart rate, atrial-ventricle synchrony and complex conditions such as avoiding pacemaker-mediated tachycardia. Through automatic model translation of abstract models to simulation-based testing and code generation for platform-level testing, this model-based design approach ensures the closed-loop safety properties are retained through the design toolchain and facilitates the development of verified software from verified models. This system is a step toward a validation and testing approach for medical cyber-physical systems with the patient-in-the-loop.

}, author = {Z. Jiang and R. Mangharam} } @conference {21, title = {SpaTeL: A Novel Spatial-temporal Logic and Its Applications to Networked Systems}, booktitle = {Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control}, year = {2015}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, keywords = {networked dynamical systems, parameter synthesis, spatial temporal logic, statistical model checking}, isbn = {978-1-4503-3433-4}, doi = {10.1145/2728606.2728633}, url = {http://doi.acm.org/10.1145/2728606.2728633}, author = {Haghighi, Iman and Jones, Austin and Kong, Zhaodan and Bartocci, Ezio and Grosu, Radu and Belta, Calin} }