Using the Virtual Heart Model to validate the mode switch pacemaker operation

摘要

This paper uses a timed-automata Virtual Heart Model to validate complex mode-switch pacemaker behavior in closed loop. Through arrhythmia case studies, it shows how formal heart-device interaction models can confirm when mode switching is necessary and whether the pacemaker responds correctly.