Simulation-Based Verification of Cardiac Pacemakers with Guaranteed Coverage

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.