Model Checking Implantable Cardioverter Defibrillators

TL;DR

This paper develops a formal hybrid system model of the human heart and implantable cardioverter defibrillator (ICD), demonstrating how model checking can verify safety properties of the device in a rigorous, mathematical framework.

Contribution

It introduces a hybrid system model of the heart-ICD loop as a STORMED system and shows how approximate reachability enables finite bisimulation, advancing formal verification methods for medical devices.

Findings

The heart-ICD system is modeled as a STORMED hybrid system.

Approximate reachability can produce finite simulations for verification.

Model checking can verify therapy-related properties in the closed loop.

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 seconds. The most 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, which improves on the existing verification procedure. In the process, we show that certain compositions respect the STORMED property. Thus it is possible to model check important formal properties of ICDs in a closed loop with the heart, such as delayed therapy, missed therapy, or inappropriately administered therapy. The results of this paper are theoretical and motivate the creation of concrete model checking procedures for STORMED systems.