Towards Model Checking of Implantable Cardioverter Defibrillators

TitleTowards Model Checking of Implantable Cardioverter Defibrillators
Publication TypeConference Paper
Year of Publication2016
AuthorsAbbas, Houssam, Jiang Kuk Jin, Jiang Zhihao, and Mangharam Rahul
Conference NameProceedings of the 19th International Conference on Hybrid Systems: Computation and Control
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-3955-1
Keywordsheart modeling, icds, life-critical cps, medical devices, stormed systems

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'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.