Closed-loop verification of medical devices with model abstraction and refinement

Abstract

This paper studies closed-loop verification of medical devices in stochastic physiological environments using a dual-chamber pacemaker case study. It builds timed-automata heart and pacemaker models in UPPAAL, applies abstraction and refinement to keep the environment both expressive and analyzable, and validates the approach on clinically relevant pacemaker-mediated tachycardia scenarios.