Model-based Design Framework for Pacemaker Software

• 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

• 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
• 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

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.

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.

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.

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

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

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.