Model-based Design Framework for Pacemaker Software

Problem Statement

Motivation

Over 600,000 cardiac medical devices recalled from 1990–2000.
40% of recent recalls were due to software issues.
It is essential to guarantee the safety and efficacy of the device software.

Cyber Physical Challenges for Medical Devices Evaluation

The Pacemaker (and other medical devices):

Autonomous device with minimum human interaction, therefore has to be able to operate under all possible conditions.
Limited diagnostic capability, inevitably leading to false-positives and false-negatives, and limited therapy capability, being able to treat the disease to a certain degree.
It is the safety of the patient we care about. Therefore the safety of the pacemaker must be evaluated in closed-loop within its environment.

pacemaker

The physical plant:

Not only the heart, but also the rest of the body.
Different dynamics even in a single patient.
Each condition has its own corresponding optimal condition.

FDA Pre-market Certification and the State-of-the-art Evaluations

Currently the US FDA requires the device manufacturers to submit proofs for:

The final product: The safety and efficacy of the device itself.
The development process: Rigorous design process which provides traceability of requirements.

Currently the device manufacturers use open-loop testing to evaluate the safety of the device and there is no formal methodologies during the design process.

The problem of traditional software development

During the past decades, pacemakers implanted into patients have recorded episodes of closed-loop interactions (Senario 1 ~ Senario N) between the heart in different conditions (Heart 1 ~ Heart N) and the pacemaker. The recordings are either appropriate pacemaker behavior in response to heart condition which all new pacemakers should also have, or inappropriate pacemaker behavior so that the new pacemakers should avoid. In order to evaluate the performance of a new pacemaker design (Pacemaker X), the inputs from the hearts in those recordings, representing different heart conditions, are fed into the new pacemaker and the outputs of the new pacemaker are compared to the recorded outputs in those senarios.

The problem of open-loop testing is that the input signals from heart do not capture the heart physiology and will not change to different pacemaker outputs. Given a closed-loop interaction between Heart i and Pacemaker i and feed its heart input signals to Pacemaker X will not capture the closed-loop behavior of Pacemaker X under heart condition i. In order to evaluate pacemaker executions under different heart conditions, especially the executions with adquate depth, there has to be a model of the heart which can capture the physiological conditions of the heart and respond to pacemaker outputs.

dev

Maintain Traceability of requirements

We developed a model-based design framework for pacemaker software. A heart model structure was designed based on the electrophysiology of the heart. At each development stage a version of the heart model is available to interact with the pacemaker model/implementation.

upp

Verification level

At verification level we have a set of non-deterministic version of our heart models with different abstraction level which covers all possible inputs to the pacemaker under different heart conditions.
Depending on the condition of the safety/efficacy properties, we choose heart model with appropirate structure and abstraction level to cover the inputs to the pacemaker under heart conditions specified in the properties.

conv

Simulation level

At Simulation level the non-determinism of our heart model are resolved by linear interpolation of the parameter ranges.
The deterministic version of our heart model responds to pacemaker pacing signals the same way as a real heart.

Implementation level

The deterministic heart model can be translated into HDL code by Mathworks HDL coder and implemented on a FPGA chip.
With appropriate analog interface, the platform can be used for closed-loop testing of pacemaker implementations.

Heart Modeling

Timed automata vs. other formalisms

We chose Timed Automata as the formalism for the heart model for several reasons:

Nondeterminism which enables model abstraction which increase coverage.
The reachability problem for timed automata is decidable, allowing us to explore the whole state space of the heart and pacemaker.
Most timing behaviors of the heart can be captured by timed automata.

The proper level of abstraction: Coverage vs. Expressiveness

In order to be used in different stages during the development process, the structure and parameters of our heart model need to be adjusted to balance between Coverage vs. Expressiveness.

Intuitively, the more complex the model is, there is more constraints on its behaviors, thus limiting its coverage. On the other hand, the added complexity allows us to capture more detailed mechanisms of the heart, allowing us to precisely model a specific heart condition. So instead of developing a single heart model, we developed a series of heart models at different abstraction levels. With Counter-Example-Guided Abstraction & Refinement (CEGAR) framework, we are able to choose the proper level of heart model abstraction during verification thus balancing coverage and expressiveness.

Heart Abstractions

Behaviorial Model of Heart Tissue

We first start with modeling the electrical behaviors of a heart tissue. A whole model of the heart consists of node automata (N0) which models the timed transitions among different time periods with different behaviors after the tissue is depolarized. The heart can then be modeled as:

where N can be arbitarily large.

Abstract conduction delay with paths

H05

Heading Sample 3

Vivamus imperdiet condimentum diam, eget placerat felis consectetur id. Donec eget orci metus, Vivamus imperdiet condimentum diam, eget placerat felis consectetur id. Donec eget orci metus, ac adipiscing nunc. Pellentesque fermentum, ante ac interdum ullamcorper. Donec eget orci metus, ac adipiscing nunc. Pellentesque fermentum, consectetur id. Donec eget orci metus, ac adipiscing nunc. Pellentesque fermentum, ante ac interdum ullamcorper. Donec eget orci metus, ac adipiscing nunc. Pellentesque fermentum, ante ac interdum ullamcorper.