Safety recalls of pacemakers and implantable cardioverter defibrillators due to firmware problems affected over 200,000 devices between 1990 and 2000, comprising 41% of the devices recalled. However, testing remains the principal means of verification in the medical device certification regime. Testing of pacemakers is performed based on a set of well understood scenarios that represent a healthy heart and common abnormalities (e.g., bradycardia). To perform testing, we need to be able to generate heart signals that correspond to each scenario, as well as provide an oracle that will tell us whether the observed behavior of the pacemaker is conformant. We designed and verified the oracle in Uppaal, before it has been systematically converted into a Stateflow model that can interact with Virtual Heart Model (VHM). Starting from pacemakers’ real-time requirements, we have extracted a set of VHM configurations that should be used for closed-loop testing of any (physical) pacemaker design.
- Miroslav Pajic