@conference {, title = {Collision-Free 3D Flocking Using the Distributed Simplex Architecture}, booktitle = {Proceedings of ISoLA Extra in Rhodes}, year = {2021}, month = {10/2021}, author = {U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller} } @article {, title = {Controllability of voltage- and calcium-driven cardiac alternans in a map model}, journal = {Chaos}, year = {2021}, author = {Munoz LM and Ampofo MO and Cherry EM} } @conference {, title = {Distributed Control for Flocking Maneuvers via Acceleration-Weighted Neighborhooding}, booktitle = {Proceedings of ACC 2021, The 2021 American Control Conference}, year = {2021}, month = {06/2021}, author = {S. Roy and U. Mehmood and R. Grosu and S. A. Smolka and S. D. Stoller and A. Tiwari} } @conference {, title = {A Distributed Simplex Architecture for Multi-Agent Systems}, booktitle = {Proceedings of SETTA 2021, Symposium on Dependable Software Engineering}, year = {2021}, month = {11/2021}, author = {U. Mehmood and S. D. Stoller and R. Grosu and S. Roy and A. Damare and S. D. Smolka} } @conference {, title = {Safe CPS from Unsafe Controllers}, booktitle = {Proceedings of CAADSPC 2001, the 2021 CPS-IoT Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems}, year = {2021}, month = {06/2021}, author = {U. Mehmood and S. Bak and S. A. Smolka and S. D. Stoller} } @booklet {, title = {Learning Distributed Controllers for V-Formation}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @booklet {, title = {Neural Flocking: MPC-based Supervised Learning of Flocking Controllers}, year = {2020}, author = {Shouvik Roy and Usama Mehmood and Radu Grosu and Scott A. Smolka and Scott D. Stoller and Ashish Tiwari} } @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} } @conference {, title = {Bisimulation in Behavioral Dynamical Systems and Generalized Synchronization Trees}, booktitle = {2018 IEEE Conference on Decision and Control (CDC)}, year = {2018}, publisher = {IEEE}, organization = {IEEE}, author = {Ferlez, James and Cleaveland, Rance and Marcus, Steven I} } @conference {, title = {Declarative vs Rule-based Control for Flocking Dynamics}, booktitle = {Proceedings of the 33rd Annual ACM Symposium on Applied Computing}, year = {2018}, publisher = {ACM}, organization = {ACM}, address = {New York, NY, USA}, isbn = {978-1-4503-5191-1}, doi = {10.1145/3167132.3167222}, url = {http://doi.acm.org/10.1145/3167132.3167222}, author = {Mehmood, Usama and Paoletti, Nicola and Phan, Dung and Grosu, Radu and Lin, Shan and Stoller, Scott D. and Tiwari, Ashish and Yang, Junxing and Smolka, Scott A.} } @article {, title = {Discordant Alternans as a Mechanism for Initiation of Ventricular Fibrillation In Vitro}, journal = {Journal of the American Heart Association}, volume = {7}, year = {2018}, month = {09}, abstract = {

Background-{\textemdash}Ventricular tachyarrhythmias are often preceded by short sequences of premature ventricular complexes. In a previous study, a restitution-based computational model predicted which sequences of stimulated premature complexes were most likely to induce ventricular fibrillation in canines in vivo. However, the underlying mechanism, based on discordant-alternans dynamics, could not be verified in that study. The current study seeks to elucidate the mechanism by determining whether the spatiotemporal evolution of action potentials and initiation of ventricular fibrillation in in vitro experiments are consistent with model predictions.

Methods and Results-{\textemdash}Optical mapping voltage signals from canine right-ventricular tissue (n=9) were obtained simultaneously from the entire epicardium and endocardium during and after premature stimulus sequences. Model predictions of action potential propagation along a 1-dimensional cable were developed using action potential duration versus diastolic interval data. The model predicted sign-change patterns in action potential duration and diastolic interval spatial gradients with posterior probabilities of 91.1\%, and 82.1\%, respectively. The model predicted conduction block with 64\% sensitivity and 100\% specificity. A generalized estimating equation logistic-regression approach showed that model-prediction effects were significant for both conduction block (P\<191015, coefficient 44.36) and sustained ventricular fibrillation (P=0.0046, coefficient, 1.63) events.

Conclusions-{\textemdash}The observed sign-change patterns favored discordant alternans, and the model successfully identified sequences of premature stimuli that induced conduction block. This suggests that the relatively simple discordant-alternans-based process that led to block in the model may often be responsible for ventricular fibrillation onset when preceded by premature beats. These observations may aid in developing improved methods for anticipating block and ventricular fibrillation. (J Am Heart Assoc. 2018;7:e007898. DOI: 10.1161/JAHA.117.007898.)

}, keywords = {alternans, arrhythmia (mechanisms), computer-based model, electrophysiology, ventricular fibrillation}, doi = {10.1161/JAHA.117.007898}, author = {Munoz, Laura and R. M. Gelzer, Anna and Fenton, Flavio and Qian, Wei and Lin, WeiYe and F. Gilmour, Robert and F. Otani, Niels} } @article {, title = {Dynamic Network Model from Partial Observations}, journal = {CoRR}, volume = {abs/1805.10616}, year = {2018}, url = {http://arxiv.org/abs/1805.10616}, author = {Elahe Ghalebi K. and Baharan Mirzasoleiman and Radu Grosu and Jure Leskovec} } @conference {, title = {Unsupervised Wafermap Patterns Clustering via Variational Autoencoders}, booktitle = {2018 International Joint Conference on Neural Networks (IJCNN)}, year = {2018}, month = {07/2018}, publisher = {IEEE}, organization = {IEEE}, address = {Rio, Brasil}, author = {Peter Tulala and Hamidreza Mahyar and Elahe Ghalebi and Radu Grosu} } @conference {, title = {Bisimulation and Hennessy-Milner Logic for Generalized Synchronization Trees}, booktitle = {Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics and 14th Workshop on Structural Operational Semantics, {EXPRESS/SOS} 2017, Berlin, Germany, 4th September 2017.}, year = {2017}, doi = {10.4204/EPTCS.255.3}, url = {https://doi.org/10.4204/EPTCS.255.3}, author = {James Ferlez and Rance Cleaveland and Steven I. Marcus} } @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} } @conference {, title = {Opacity for switched linear systems: Notions and characterization}, booktitle = {2017 IEEE 56th Annual Conference on Decision and Control (CDC)}, year = {2017}, month = {Dec}, keywords = {allowed switching sequences, directed graph, directed graphs, discrete time systems, discrete-time switched linear systems, linear systems, Mathematical model, Power systems, switched linear systems, Switched systems, Switches, switching systems (control)}, doi = {10.1109/CDC.2017.8264445}, author = {B. Ramasubramanian and R. Cleaveland and S. I. Marcus} } @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} } @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} } @article {, title = {Computing Compositional Proofs of Input-to-Output Stability Using SOS Optimization and δ-Decidability}, journal = {Nonlinear Analysis: Hybrid Systems}, year = {2016}, month = {05/2016}, author = {A. Murthy and Md. A. Islam, and S. A. Smolka and R. Grosu} } @conference {, title = {Experience Report: Model-Based Test Automation of a Concurrent Flight Software Bus}, booktitle = {2016 IEEE 27th International Symposium on Software Reliability Engineering (ISSRE)}, year = {2016}, month = {Oct}, keywords = {aerospace computing, API, application program interfaces, Automation, Computer architecture, Concurrency, Concurrent computing, concurrent design, concurrent flight software bus, concurrent publisher-subscriber architecture style, concurrent system testing, Context, Flight Software, MBT technique, message passing, Microsoft Spec Explorer MBT tool, middleware, Model Based Testing, model-based test automation, NASA, NASA Core Flight Software software bus module, program testing, Publish-Subscribe, safety-critical software, safety-critical system, Software, software architecture, SUT, system-under-test, test case analysis, Testing}, doi = {10.1109/ISSRE.2016.47}, author = {D. Ganesan and M. Lindvall and S. Hafsteinsson and R. Cleaveland and S. L. Strege and W. Moleski} } @conference {, title = {A framework for decentralized opacity in linear systems}, booktitle = {2016 54th Annual Allerton Conference on Communication, Control, and Computing (Allerton)}, year = {2016}, month = {Sept}, keywords = {adversarial observer, colluding adversary, Computers, cyber-physical system, Cyber-physical systems, decentralized opacity, directed graph, directed graphs, ISO, linear system, linear systems, observers, Power systems, Trajectory}, doi = {10.1109/ALLERTON.2016.7852240}, author = {B. Ramasubramanian and R. Cleaveland and S. I. Marcus} } @conference {, title = {A framework for opacity in linear systems}, booktitle = {2016 American Control Conference, {ACC} 2016, Boston, MA, USA, July 6-8, 2016}, year = {2016}, doi = {10.1109/ACC.2016.7526666}, url = {https://doi.org/10.1109/ACC.2016.7526666}, author = {Bhaskar Ramasubramanian and Rance Cleaveland and Steven I. Marcus} } @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} } @article {, title = {Model-Order Reduction of Ion Channel Dynamics Using Approximate Bisimulation}, journal = {Theoretical Computer Science}, volume = {599C}, year = {2015}, month = {09/2015}, chapter = {34}, author = {Md. A. Islam and A. Murthy and E. Bartocci and E. M. Cherry and F. H. Fenton and J. Glimm and S. A. Smolka and R. Grosu} } @conference {, title = {UML-VT: A Formal Verification Environment for UML Activity Diagrams.}, booktitle = {P\&D@ MoDELS}, year = {2015}, author = {Daw, Zamira and Mangino, John and Cleaveland, Rance} }