Medical Device Validation & Verification


In this project we adapted a Model Based Design framework to ensure the safety of medical device software and we use implantable pacemaker as case study.

Related Projects:

  • Pacemaker Verification
    Incorporating model checking techniques to evaluate both Safety and Efficacy of pacemaker algorithms
  • Penn Virtual Heart Model (VHM)
    The VHM models the Electrophysiology of the heart. It can simulate Electrogram signals for different clinical cases and respond to external pacing signals.
  • Multi-Level Model Translation
    An integrated tool chain from model to implementation, which ensures equivalence among models at different level so that key properties are preserved.


Other Members:

  • Miroslav Pajic
  • Sriram Radhakrishnan
  • Varun Sampath
  • Shilpa Sarode

Video Explanation:

  • The "Heart On a Chip (HOC)" demo video describes how we implemented our Virtual Heart Model on to a FPGA chip and interact with a real pacemaker in real-time. The HOC platform bridges the gap between model simulation and physical testing thus can play a very important role during the device certification process. More details can be found in Heart On a Chip website.
  • The "SEAS Pacemaker" video was recorded during the 2012 Penn SEAS Senior Design Competition. The Pacemaker Verification System (PVS) team from mLab demonstrated their implementation of Penn Virtual Heart Model on a FPGA board and interact with a commercial pacemaker in real-time. They ended up in the 1st place in the competition. Congratulations to Siriram, Varun and Shilpa!
  • The"Penn Virtual Heart Model" video was recorded back in 2009 but still explained the main contributions of our Virtual Heart Model.
  • Reentry circuit is the primary source for Cardiac Arrhythmia. The "VHM v2.0 Atrial Flutter Simulation" video shows the capability of our Virtual Heart Model to model this complex structure, and its response to physician's inputs during Electrophysiology Study. More information can be found in the case studysection.
Current Members
Profile photo of Zhihao Jiang
Zhihao Jiang
Rahul Mangharam's Profile Photo
Rahul Mangharam
Modeling and Verification of a Dual Chamber Implantable Pacemaker (Article)
Jiang, Zhihao; Pajic, Miroslav; Moarref, Salar; Alur, Rajeev; Mangharam, Rahul

18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 7214, Page(s): 188-203, 2012.