FAQs

The questions below are provided by the Pacemaker Challenge community.

General

1. What needs have you addressed?

Our work aims to increase the confidence on safety and efficacy of the device itself and its development process while reducing the cost due to revisions during the development process. Our research has three outcomes:

  • Reduced the effort for evaluation of closed-loop safety of the device software. This is achieved via an end-to-end verification, simulation-based testing and platform testing model-based tool chain.
  • Improved dynamic system testing with interactions between the pacemaker and the heart model. We have developed an integrated functional and formal heart model to interact with the pacemaker.
  • Provide a Model-based Development Toolchain to increase the confidence of the medical device software development process.
To get a quick overview of our work please watch this short video on the Heart-on-a-Chip.

2. Who are your target readers? From which domain?

  • Software engineers overseeing requirements, specification and testing in medical device manufacturing companies
  • Regulatory authorities such as the US Food and Drug Administration (FDA) for medical device software development process improvements
  • Cardiac rhythm therapy algorithm designers from both academia and industry.

3. What is the technology readiness level of your approach?

Our Heart-on-a-Chip, Virtual Heart Model, Model Checking and end-to-end Model-based Design testing approach have been designed, published and are currently in the prototyping phase. This puts us in the TR4 level of readiness according to the DoE Technology Readiness Assessment Guide (page 9)

4. How much time was spent to produce the solution?

We have invested 4 years with two productive Ph.D. students in this project.

Scope

1. Which parts of the pacemaker specification did you consider?

Our focus has been on establishing high confidence in the system software and the software development process of the pacemaker. We have developed the following component evaluations:

  • Sensing and actuation - established safety criteria for the basic timing cycles and the effect of noise in sensing, lead placement, lead dislodgment and failure to sense/pace on the timing behaviors of the pacemaker software.
  • Pacemaker software - established correctness of different timers in the pacemaker
  • Pacemaker parameter settings - timing parameters such as Lower Rate Interval, Upper Rate Interval, A-V interval, Refractory periods, etc.

2. What aspects did you consider? (e.g. System level / Hardware / Software)

We considered software and system level safety within the closed loop context of the pacemaker and heart.
  • Virtual Heart Model - We have developed a Timed Automata model of the heart to interact with the pacemaker. The model incorporates the electro-physiological function of the heart. The heart model provides both functional (electrogram signals) and formal (timing events) interfaces to pacemaker models. The VHM has also been implemented in Matlab and Simulink for simulation-based testing. We have a working Heart-on-a-Chip platform for closed-loop testing with real pacemakers at the University of Pennsylvania. See details at http://pvs.medcps.org/
  • Pacemaker Model Verification and Translation - We have implemented a model of the pacemaker with all the timers to satisfy the Boston Scientific specification. This model was implemented in UPPAAL (model checker for timed automata models). The verified model was then automatically translated to Stateflow/Simulink by the UPP2SF model translation tool. The tool, which was developed by us, preserves the properties proven in the verified model to Staflow's loose semantics.
  • Pacemaker Tester - We implemented a large set of Medtronic timing tests. These are implemented on a hardware platform and automatically test real pacemaker hardware.
  • Automated Code-generation of Verified Models - Stateflow/Simulink models are used to automatically generate pacemaker code for a variety of microcontroller architectures.

3. Which parts of the environment have you modeled?

  • Virtual Heart Model - It is important to verify and test the closed-loop heart and pacemaker system. We have a heart model to interface with pacemaker models (Timed Automata, Stateflow/Simulink), pacemakers implemented on microcontroller platforms and also real pacemakers manufactured by Boston Scientific, Medtronic and St. Jude. Currently the heart model covers the following electrophysiological arrhythmias:
    • Normal Sinus Rhythm
    • Bradycardia
    • Heart block
    • Supraventricular Tachycardia
    • Lead displacement
    • Lead Cross-talk and race conditions
    • Pacemaker Mediated Tachycardia
    • The heart model has a common kernel and exposes a functional interface} for both simulation-based and platform testing. It also exposes a formal interface of the event timing for verification of the pacemaker timing properties.
  • Blood-oxygen Physiological Modeling: For quantative verification of the closed-loop system with costs such as efficacy of therapy and device energy consumption, we have developed parts of the blood-oxygen model which interfaces with the heart and pacemaker closed-loop system. This way, we can evaluate the effectiveness of therapies related to rate-response, pacemaker mediated tachycardia and newer algorithms.

4. Which process phases have you considered?

We focus on the requirement specification, software design, testing for certification. Our primary contribution is the development of an end-to-end model-based design approach for rapid certification of the design process. This incorporates:
  • Formal Modeling of the Heart - timing behaviors of electric conduction of the heart are modeled by a network of timed automata. This helps us to specify requirements for pacemaker under specific heart conditions.
  • Formal Modeling of the Pacemaker - majority of timing aspects in the Boston Scientific pacemaker specification are implemented using timed automata. Timing properties have been checked and verified.
  • Model Translation of Verified Pacemaker Models - Automated translation of UPPAAL timed automata pacemaker model to Stateflow/Simulink while preserving verified timing properties.
  • Simulation-based Testing of the Closed-loop system - Detailed heart model has also been implemented in Matlab and Simulink and interfaces with the pacemaker Stateflow/Simulink model.
  • Code-generation of Verified Pacemaker Model - From the above pacemaker model we have generated code for a variety of microcontroller architectures.
  • Closed-loop Platform Testing - The Heart-on-a-Chip platform incorporates the Virtual Heart Model implemented on an FPGA hardware platform and interfaces with an automated hardware tester for timing analysis. It also interfaces with real pacemakers for closed-loop platform testing.

Modeling

1. What modeling formalisms did you use? Why?

Timed Automata and the Mathworks toolchain. The reasons for using timed automata are:

  • Timed automata is suitable for modeling timing behaviors of a system. The coordinated contractions of the heart are based on timing behaviors of its electrical activities, which makes timed automata a good formalism to model both the heart and the pacemaker.
  • Timed automata is well studied and tools like UPPAAL are available and mature.
  • Most pacemaker functions we would like to cover can be modeled by timed automata
We also use the Mathworks Stateflow/Simulink/Embedded Coder toolchain as it is practical and is widely used in industry. All models and tools are publicly available. The implementation is clean and moderately easy to adopt. The model is scalable which allows for more than enough refinement to check a large variety of common properties. See publications for more details.

2. Are the formalisms used rigorous?

Timed automata is a rigorous formulation.

3. How accessible are the modeling methods and notations for practicing engineers? (e.g. need training, fairly accessible)

Timed automata is an extension of state machine with real-time clocks, which is intuitive for engineers. The tools and Temporal Logic are intuitive to learn with minimal training.

4. Which aspects did you not model? Why?

  • On the heart side: We did not model non-timing related properties such as the mechanical contractions of the heart muscle. The performance of heart pumping can be inferred by the electrical behaviors of the heart (i.e. which is how the pacemaker interacts with the heart). This point is shown to be valid in the Cardiac Electrophysiology domain.
  • On the pacemaker side: We did not model pacemaker components other than the core diagnosis/therapy software. We only focused on potential safety violations caused by the diagnosis/therapy software. The interaction between the diagnosis/therapy software and the rest of the pacemaker can be isolated by safety protocols thus the rest of the pacemaker has little impact on the safety of the diagnosis/therapy software.

5. What are the most difficult aspects to model?

  • On the heart side: How to use abstraction to cover different heart conditions and refine the heart model to pinpoint a specific heart condition. We have implemented a Counter-Example Guided Abstraction Refinement (CEGAR) methodology to verify complex closed-loop properties such as Endless-loop Tachycardia (pacemaker mode switch operation) and Pacemaker Mediated Tachycardia.
  • On the pacemaker side: Advanced features which operate on heart condition history. Some of them cannot be modeled using Timed Automata.

6. What is the cost of the modeling?

All our models, code and platforms are publicly available for the research community. The UPPAAL tool is free and open sourced. Mathworks tools require a license to be purchased. The models themselves are easy to use and require less than a week's effort by a software engineer with 5 years of experience.

Verification & Validation

1. What properties have you verified?

We have verified safety properties regarding avoidance of unsafe closed-loop states (i.e. low heart rate, paced high heart rate) and unsafe closed-loop executions (i.e. existence of Pacemaker Mediated Tachycardia).

2. What properties could be ensured by construction?

Timing and correctness of software properties are verified at the abstract pacemaker model level. These properties are maintained in the Stateflow/Simulink by the UPP2SF model translation tool. The verified models are used to generate operational pacemaker code. Thus, our end-to-end model-based toolchain allows us to proceed from verified models to verified code.

3. What methods did you use for the verification?

Model checking of timed automata models.

4. How accessible are the verification methods for practicing engineers?

Fairly accessible.

5. How did you validate the system?

The heart model was based on techniques and terminologies used during clinical practices and the model has been validated by the Director of Cardiac Electrophysiology of the Philadelphia VA Hospital and the University of Pennsylvania Hospital. These hospitals are among the top hospitals responsible for the most cardiac ablation and cardiac device implants in the US. We have also demonstrated that our model captures the timing behaviors of a real hearts (given the same input signals.) See Atrial Flutter video here

6. Is the functional design verified against the requirements specification? How complete?

Yes. For each timing cycle of the pacemaker we specified a property to verify whether the requirement has been satisfied.

7. Have you simulated the model?

Yes. The models of the closed-loop system have been simulated both in model checker (UPPAAL) and Simulink.

Tools

1. Which tools did you use? What is their maturity?

  • Verification: we use model checker UPPAAL. It is a mature tool that has been used for various applications.
  • Model Translation: from UPPAAL to Simulink we use UPP2SF which is developed by Pajic et.al. The tool is not fully automated yet and requires some manual effort.
  • Simulation & Code Generation: we use Matlab/Simulink which is widely adopted by both academia and industry. Even though Stateflow does not have formal semantics the UPP2SF tool ensures verified properties are maintained and the practicality of using Mathworks tools makes it more available than academic tools for code generation.

2. How much expertise is expected from the users of these tools?

For UPPAAL, the user needs to know basic state transition system and the ability to specify requirements using temporal logic. For Matlab/Simulink the user requires basic understanding of programming and syntax of Simulink.

Certification

1. What aspects of the functional safety certification did you cover?

None.

2. How have you used this challenge?

I personally have used the challenge as a case study of my research for developing a model-based design framework for Cyber-Physical Systems like medical devices.
  • The Heart-on-a-Chip platform won the First Prize in the 9th World Embedded Systems Competition (Medical Devices category), Seoul, Korea 2012.
  • Our work has won the Best Student Paper Award in the 2012 Real-Time System Conference (RTAS) at CPSWeek 2012.
  • Our work was nominated for Best Paper at TACAS 2012.
Several research groups are using our models and tools. These include Marta Kwiatkowska, University of Oxford and Sanjit Seshia, UC Berkeley, etc. The models have been downloaded over 100 times in the past year.