Indian Journal of Science and Technology
DOI: 10.17485/ijst/2017/v10i20/104028
Year: 2017, Volume: 10, Issue: 20, Pages: 1-12
Original Article
Syed Asad Raza Kazmi1*, Sana Abubakkar1 , Awais Qasim1 , Syed Hassan Abbas Kazmi2 and Usman Qamar Qureshi3
1Department of Computer Science, Government College University, Katchery Road, Lahore – 54000, Pakistan; [email protected], [email protected], [email protected] 2King Edward Medical University, Nelagumbad, Mayo Hospital Road, Lahore – 54000, Pakistan; [email protected] 3Nishtar Medical College, Multan – 60000, Pakistan; [email protected]
*Author for the correspondence:
Syed Asad Raza Kazmi
Department of Computer Science, Government College University, Katchery Road, Lahore – 54000, Pakistan; [email protected]
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.
Keywords: Formal Modelling, Pacemaker Modelling, Pacemaker Systems, Temporal Modelling
Subscribe now for latest articles and news.