{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T22:35:50Z","timestamp":1777761350501,"version":"3.51.4"},"reference-count":53,"publisher":"Emerald","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,12,10]]},"abstract":"<jats:p>The design of bug-free and safe medical device software is challenging, especially in complex implantable devices. This is due to the device\u2019s closed-loop interaction with the patient\u2019s 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.<\/jats:p>\n                  <jats:p>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.<\/jats:p>\n                  <jats:p>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\u2019s 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.<\/jats:p>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1561\/1000000040","type":"journal-article","created":{"date-parts":[[2015,12,10]],"date-time":"2015-12-10T06:23:13Z","timestamp":1449728593000},"page":"309-391","source":"Crossref","is-referenced-by-count":5,"title":["High-Confidence Medical Device Software Development"],"prefix":"10.1108","volume":"9","author":[{"given":"Zhihao","family":"Jiang","sequence":"first","affiliation":[{"name":"University of Pennsylvania ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Mangharam","sequence":"additional","affiliation":[{"name":"University of Pennsylvania ,","place":["USA"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"140","published-online":{"date-parts":[[2015,12,10]]},"reference":[{"key":"2026032901221020500_ref001","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A Theory of Timed Automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoretical Computer Science"},{"key":"2026032901221020500_ref002","first-page":"3","article-title":"In Silico Preclinical Trials: A Proof of Concept in Closed-Loop Control of Type 1 Diabetes","volume-title":"Journal of Diabetes Science and Technology","author":"Kovatchev","year":"2009"},{"key":"2026032901221020500_ref003","first-page":"268","article-title":"A Model Study of Changes in Excitability of Ventricular Muscle Cells","volume-title":"American Journal of Physiology","author":"Beaumont","year":"1995"},{"key":"2026032901221020500_ref004","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","article-title":"A Tutorial on UPPAAL","volume-title":"Formal Methods for the Design of Real-Time Systems, Lecture Notes in Computer Science","author":"Behrmann","year":"2004"},{"issue":"1s","key":"2026032901221020500_ref005","doi-asserted-by":"crossref","DOI":"10.1145\/2435227.2435246","article-title":"Pacemaker control of heart rate variability: A cyber physical system perspective","volume":"12","author":"Bogdan","year":"2013","journal-title":"ACM Transactions on Embedded Computing Systems"},{"key":"2026032901221020500_ref006","article-title":"PACEMAKER System Specification. Boston Scientific","volume-title":"Device Documentation","author":"Boston Scientific Corporation","year":"2007"},{"key":"2026032901221020500_ref007","article-title":"The Compass - Technical Guide to Boston Scientific Cardiac Rhythm Management Products","volume-title":"Device Documentation","author":"Boston Scientific Corporation","year":"2007"},{"issue":"5","key":"2026032901221020500_ref008","doi-asserted-by":"crossref","first-page":"752","DOI":"10.1145\/876638.876643","article-title":"Counter Example-Guided Abstraction Refinement for Symbolic Model Checking","volume":"50","author":"Clarke","year":"2003","journal-title":"Journal of the ACM"},{"key":"2026032901221020500_ref009","first-page":"52","volume-title":"Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic","author":"Clarke","year":"1982"},{"issue":"5","key":"2026032901221020500_ref010","doi-asserted-by":"crossref","first-page":"1512","DOI":"10.1145\/186025.186051","article-title":"Model Checking and Abstraction","volume":"16","author":"Clarke","year":"1994","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"2026032901221020500_ref011","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1111\/j.1525-1594.2008.00620.x","article-title":"Deep brain stimulation devices: A brief technical history and review","volume":"33","author":"Coffey","year":"2009","journal-title":"Artificial Organs"},{"key":"2026032901221020500_ref012","volume-title":"Medical Devices Software: Verification, Validation and Compliance","author":"Vogel","year":"2011"},{"issue":"4","key":"2026032901221020500_ref013","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1081\/JCMR-100108588","article-title":"Myocardial fiber orientation mapping using reduced-encoding diffusion tensor imaging","volume":"3","author":"Hsu","year":"2011","journal-title":"Journal of Cardiovascular Magnetic Resonance"},{"key":"2026032901221020500_ref014","volume-title":"System architecture virtual integration: A case study","author":"Feiler","year":"2010"},{"key":"2026032901221020500_ref015","article-title":"Design Control Guidance For Medical Device Manufacturers","volume-title":"Center for Devices and Radiological Health","author":"U. S. Food and Drug Administration","year":"1997"},{"key":"2026032901221020500_ref016","article-title":"General principles of software validation; final guidance for industry and fda staff","volume-title":"Center for Devices and Radiological Health","author":"U. S. Food and Drug Administration","year":"2002"},{"key":"2026032901221020500_ref017","article-title":"Guidance for the Content of Premarket Submissions for Software Contained in Medical Devices","volume-title":"Center for Devices and Radiological Health","author":"U. S. Food and Drug Administration","year":"2005"},{"key":"2026032901221020500_ref018","article-title":"Ensuring the Safety of Marketed Medical Devices: CDRH\u2019s Medical Device Postmarket Safety Program","volume-title":"Center for Devices and Radiological Health","author":"U. S. Food and Drug Administration","year":"2006"},{"key":"2026032901221020500_ref019","article-title":"Medical device recall report - fy2003 to fy2012","volume-title":"Center for Devices and Radiological Health","author":"U. S. Food and Drug Administration","year":"2012"},{"key":"2026032901221020500_ref020","article-title":"Classification of medical devices","volume-title":"US FDA documents","author":"U. S. Food and Drug Administration","year":"2014"},{"key":"2026032901221020500_ref021","article-title":"Pacemaker Lead Displacement: Mechanisms And Management","volume-title":"Indian Pacing Electrophysiology Journal","author":"Fuertes","year":"2003"},{"issue":"4","key":"2026032901221020500_ref022","doi-asserted-by":"crossref","first-page":"486","DOI":"10.1111\/j.1540-8159.1982.tb02265.x","article-title":"Endless loop tachycardia in an av universal (ddd) pacemaker","volume":"5","author":"Furman","year":"1982","journal-title":"Pacing and Clinical Electrophysiology"},{"key":"2026032901221020500_ref023","article-title":"Autosar\u2013a worldwide standard is on the road","volume":"62","author":"F\u00fcrst","year":"2009","journal-title":"14th International VDI Congress Electronic Systems for Vehicles"},{"key":"2026032901221020500_ref024","first-page":"1","volume-title":"A cyber-physical system approach to artificial pancreas design","author":"Ghorbani","year":"2013"},{"key":"2026032901221020500_ref025","first-page":"396","volume-title":"Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science","author":"Grosu","year":"2011"},{"key":"2026032901221020500_ref026","unstructured":"Mathworks Inc\n          . Matlab R2011a Stateflow Documentation. http:\/\/www.mathworks.com\/help\/toolbox\/stateflow, 2016."},{"key":"2026032901221020500_ref027","first-page":"243","volume-title":"Compositionality results for cardiac cell dynamics","author":"Islam","year":"2014"},{"key":"2026032901221020500_ref028","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/MC.2006.113","article-title":"A Formal Methods Approach to Medical Device Review","volume":"39","author":"Jetley","year":"2006","journal-title":"IEEE Computer"},{"key":"2026032901221020500_ref029","first-page":"263","volume-title":"Modeling Cardiac Pacemaker Malfunctions with the Virtual Heart Model","author":"Jiang"},{"key":"2026032901221020500_ref030","unstructured":"Z.\n              Jiang\n             and R.Mangharam. Virtual Heart Model website - http:\/\/medcps.org, 2016."},{"key":"2026032901221020500_ref031","first-page":"239","volume-title":"Real-time heart model for implantable cardiac device validation and verification","author":"Jiang"},{"key":"2026032901221020500_ref032","doi-asserted-by":"crossref","DOI":"10.1109\/ICCPS.2011.28","volume-title":"Model-based Closed-loop Testing of Implantable Pacemakers","author":"Jiang","year":"2011"},{"key":"2026032901221020500_ref033","first-page":"122","volume-title":"Cyber-Physical Modeling of Implantable Cardiac Medical Devices","author":"Jiang"},{"key":"2026032901221020500_ref034","first-page":"188","article-title":"Modeling and Verification of a Dual Chamber Implantable Pacemaker","volume":"7214","author":"Jiang","year":"2012","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"issue":"2","key":"2026032901221020500_ref035","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s10009-013-0289-7","article-title":"Closed-loop verification of medical devices with model abstraction and refinement","volume":"16","author":"Jiang","year":"2014","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"2026032901221020500_ref036","unstructured":"Z.\n              Jiang\n            , H.Abbas, P.J.Mosterman, and R.Mangharam. Tech Report: Abstraction-Tree For Closed-loop Model Checking of Medical Devices. http:\/\/repository.upenn.edu\/mlab_papers\/73, 2015."},{"key":"2026032901221020500_ref037","volume-title":"Clinical Cardiac Electrophysiology","author":"Josephson","year":"2008"},{"key":"2026032901221020500_ref038","first-page":"134","article-title":"UPPAAL in a Nutshell","volume-title":"International Journal on Software Tools for Technology Transfer (STTT)","author":"Larsen","year":"1997"},{"issue":"7","key":"2026032901221020500_ref039","doi-asserted-by":"crossref","DOI":"10.1001\/jama.286.7.793","article-title":"Recalls and Safety Alerts involving Pacemakers and Implantable Cardioverter-Defibrillator Generators","volume":"286","author":"Maisel","year":"2001","journal-title":"JAMA"},{"issue":"2","key":"2026032901221020500_ref040","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1109\/TCBB.2012.125","article-title":"Curvature analysis of cardiac excitation wavefronts","volume":"10","author":"Murthy","year":"2013","journal-title":"IEEE\/ACM Transactions on Computational Biology and Bioinformatics"},{"key":"2026032901221020500_ref041","volume-title":"Nano-RK Sensor RTOS","author":"Nano-RK","year":"2007"},{"key":"2026032901221020500_ref042","first-page":"173","volume-title":"From Verification to Implementation: A Model Translation Tool and a Pacemaker Case Study","author":"Pajic","year":"2012"},{"issue":"4s","key":"2026032901221020500_ref043","doi-asserted-by":"crossref","DOI":"10.1145\/2584651","article-title":"Safety-critical medical device development using the upp2sf model translation tool","volume":"13","author":"Pajic","year":"2014","journal-title":"ACM Transactions on Embedded Computing Systems"},{"issue":"2","key":"2026032901221020500_ref044","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1016\/0021-9991(89)90213-1","article-title":"A three-dimensional computational method for blood flow in the heart. 1. immersed elastic fibers in a viscous incompressible fluid","volume":"81","author":"Peskin","year":"1989","journal-title":"Journal of Computer Physics"},{"key":"2026032901221020500_ref045","first-page":"119","volume-title":"Active strain and activation models in cardiac electromechanics","author":"Rossi","year":"2011"},{"issue":"1","key":"2026032901221020500_ref046","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/s10439-007-9405-8","article-title":"Electrophysiological modeling of fibroblasts and their interaction with myocytes","volume":"36","author":"Sachse","year":"2008","journal-title":"Annals of Biomedical Engineering"},{"key":"2026032901221020500_ref047","article-title":"Killed by Code: Software Transparency in Implantable Medical Devices","volume-title":"Software Freedom Law Center","author":"Sandler","year":"2010"},{"key":"2026032901221020500_ref048","doi-asserted-by":"crossref","DOI":"10.1016\/j.jacc.2004.10.045","article-title":"Current of injury predicts adequate active lead fixation in permanent pacemaker\/defibrillation leads","volume-title":"Journal of the American college of Cardiology","author":"Saxonhouse","year":"2005"},{"key":"2026032901221020500_ref049","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1515\/bmte.2001.46.s2.26","article-title":"Creation of a Human Heart, Model and its Customisation using Ultrasound Images","volume":"46","author":"Schulte","year":"2001","journal-title":"Biomedizinische Technik\/Biomedical Engineering"},{"issue":"2","key":"2026032901221020500_ref050","first-page":"209","article-title":"Advances in modeling ventricular arrhythmias: from mechanisms to the clinic","volume":"6","author":"Trayanova","year":"2014","journal-title":"Wiley Interdisciplinary Reviews: Systems Biology and Medicine"},{"key":"2026032901221020500_ref051","volume-title":"Human Subject Protection; Acceptance of Data from Clinical Studies for Medical Devices; Proposed Rule","author":"U. S. Food and Drug Administration","year":"2013"},{"key":"2026032901221020500_ref052","first-page":"6","article-title":"Timed Weak Simulation Verification and its Application to Stepwise Refinement of Real Time Software","volume-title":"International Journal of Computer Science and Network Security","author":"Yamane","year":"2006"},{"issue":"5","key":"2026032901221020500_ref053","doi-asserted-by":"crossref","first-page":"e0125987","DOI":"10.1371\/journal.pone.0125987","article-title":"Recalls of cardiac implants in the last decade: what lessons can we learn?","volume":"10","author":"Zhang","year":"2015","journal-title":"PLoS ONE"}],"container-title":["Foundations and Trends\u00ae in Electronic Design Automation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/9\/4\/309\/10913518\/1000000040en.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/www.emerald.com\/fteda\/article-pdf\/9\/4\/309\/10913518\/1000000040en.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T14:13:38Z","timestamp":1777472018000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.emerald.com\/fteda\/article\/9\/4\/309\/1321577\/High-Confidence-Medical-Device-Software"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,10]]},"references-count":53,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2015,12,10]]}},"URL":"https:\/\/doi.org\/10.1561\/1000000040","relation":{},"ISSN":["1551-3939","1551-3947"],"issn-type":[{"value":"1551-3939","type":"print"},{"value":"1551-3947","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,12,10]]}}}