New Insights Into Soft-Faults Induced Cardiac Pacemakers Malfunctions Analyzed at System-Level via Model Checking

Progressive shrinking of CMOS device sizes has permitted reductions in power consumption and miniaturization of electronic devices. In parallel, modern pacemakers implemented with advanced technologies have proved to be more sensitive than earlier models to soft errors induced notably by external radiations. Traditionally, the analysis of the impact of soft faults (SFs), such as those induced by single-event upsets, on the behavior of pacemaker devices, has been carried out by dynamic radiation ground testing and clinical observations. However, these techniques are expensive. They can only be done very late in the design cycle, after the design is manufactured and in part after it is implanted. This paper presents a new model-based analysis of the impact of SFs on the behavior of cardiac pacemakers at a system level. It is performed by: 1) introducing a new probabilistic timed automata (PTA) model; 2) verifying this model against a set of functional properties to ensure it meets its specifications under normal conditions; 3) applying a new methodology to inject SFs at a certain time in the PTA model of the pacemaker and to verify their impact on the pacemaker's behavior is introduced; and 4) identifying different scenarios for SFs that may lead to malfunction, including oversensing, undersensing, and output failure. The reported formal modeling is done in PRISM and the analysis is done with the Storm model checker.