Simulation-Based Verification of Cardiac Pacemakers with Guaranteed Coverage

Zhenqi Huang, Chuchu Fan, Alexandru Mereacre, Sayan Mitra, Marta Kwiatkowska

Research output: Contribution to journalArticlepeer-review


A framework based on discrepancy functions is proposed for investigating and validating the time-bounded safety properties. The approach builds on algorithms that cover a set of model behaviors from a single simulation of the model. The first step for model-based design and analysis is to construct a model of the system. The key component of our framework is a hybrid I/O automaton (HIOA), a (possibly nondeterministic and nonlinear) state machine whose state variables evolve discretely and continuously. The discrete transitions are written in the usual precondition-effect style and the continuous evolution is described by differential and algebraic equations. The solutions of these equations are called trajectories. An execution of a hybrid automaton records the evolution of the variables for a particular choice of the initial state and all other parameters of the model. Using C2E2 and the Matlab-based implementation of the algorithms, a number of properties can be verified for several different models of the pacemaker-heart system. The simulation-based verification technology for nonlinear hybrid systems is poised to take on the challenges in design and analysis of medical devices, providing a rigorous foundation for methodologies needed for their verification and certification.

Original languageEnglish (US)
Article number7130608
Pages (from-to)27-34
Number of pages8
JournalIEEE Design and Test
Issue number5
StatePublished - 2015

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering


Dive into the research topics of 'Simulation-Based Verification of Cardiac Pacemakers with Guaranteed Coverage'. Together they form a unique fingerprint.

Cite this