Formal Modelling and Verification of the Operational Modes of Pacemaker

Objectives: The importance of error free smooth functioning of the heart pacemaker in providing consistent relief to the heart patients has pushed the researchers to devise highly refined bug free devices. Pacemaker is an important safety critical device that is used to keep the heartbeat uniform in patients with low heartbeat. Since the smooth functioning of the pacemaker is responsible to provide oxygen and nutrients to the whole body of the patient in an appropriate ratio, therefore, any conflict in the device would be life threatening. It is therefore extremely necessary to ensure the error free working of such critical health device. Methods: Previously, different verification methods have been employed to design and verify safety critical devices with varying degree of reliability and reproducibility. Keeping in view the specifications of the pacemaker, this paper presents a model for the verification and validation of a pacemaker system using the SPIN model checker. Findings: The LTL formulas are characterized to handle the uncertainty or any abnormal activity during the process. The system model is designed using SPIN model checker in which different LTL properties are verified. A theoretical description is supported by some experimental results, generated using the existing logics and techniques. Application: This work can be further enhanced for the formal verification of critical medical equipment to ensure their correct functioning.