Total views : 86

Formal Modelling and Verification of the Operational Modes of Pacemaker


  • Department of Computer Science, Government College University, Katchery Road, Lahore – 54000, Pakistan
  • King Edward Medical University, Nelagumbad, Mayo Hospital Road, Lahore – 54000, Pakistan
  • Nishtar Medical College, Multan – 60000, Pakistan


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.


Formal Modelling, Pacemaker Modelling, Pacemaker Systems, Temporal Modelling.

Full Text:

 |  (PDF views: 88)


  • Edmund MC, Jeannette MW. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR). 1996 Dec; 28(4):626–43. CrossRef.
  • Zhihao J, Miroslav P, Rajeev A, Rahul M. Closed-loop verification of medical devices with model abstraction and refinement. International Journal on Software Tools for Technology Transfer. 2014 Apr; 16(2):191–213. CrossRef.
  • Karen S, Lysandra O, Laura M, Robert M. Killed by code: Software transparency in implantable medical devices. Software Freedom Law Center. 2010 Jul; 308-319.
  • Awais Q, Asad RK, Ilyas F. Executable Semantics for the Formal Specification and Verification of E-agents. Indian Journal of Science and Technology. 2015 Jul; 8(16):1–8.
  • Awais Q, Asad RK, Ilyas F. Formal specification and verification of real-time multi-agent system using timed Arc Petri Nets. Advances in Electrical and Computer Engineering. 2015 Jan; 15(3):73–8. CrossRef.
  • Insup L, George JP, Rance C, John H, Bruce HK, Peter L, Harvey R, Lui S. High-confidence medical device software and systems. Computer Application. 2006 Apr; 39(4):33–8. CrossRef.
  • Artur OG, Marcel O. Formal development of a cardiac pacemaker: from specification to code. Brazilian Symposium on Formal Methods, Springer Berlin Heidelberg; 2010. p. 210–25.
  • William HM, Michael OS, William GS, Kristin E, Laurence ME. Recalls and safety alerts involving pacemakers and implantable cardioverter-defibrillator generators. 2001 Aug; 286(7):793–9.
  • Daniel H, Thomas S, Kevin F, Tadayoshi K, William HM. Security and privacy for implantable medical devices. IEEE pervasive computing. 2008 Jan; 7(1):1–7.
  • Àdàm B, Arnold P, Àdàm S, Istvan P. Clinical Observations with Longterm Atrial Pacing. Pacing and clinical electrophysiology. 1998 Jan; 21(1):246–9. CrossRef.
  • Anthony H. Seven myths of formal methods. IEEE software. 1990 Sep; 7(5):11–9. CrossRef.
  • Dominique M, Bernhard S, Alan W. The Pacemaker Challenge: Developing Certifiable Medical Devices. Dagstuhl Reports, Germany: 2014.
  • Lee I, Sokolsky O, Chen S, Hatcliff J, Jee E, Kim B, King A, Mullen-Fortino M, Park S, Roederer A, Venkatasubramanian KK. Challenges and research directions in medical cyber–physical systems. Proceedings of the IEEE. 2012; 100(1):75–90. CrossRef.
  • Jos CMB. A brief history of process algebra. Theoretical Computer Science. 2005 May; 335(2-3):131–46. CrossRef.
  • Steve S. An operational semantics for timed CSP. Information and computation. 1995 Feb; 116(2):193–213. CrossRef.
  • Awais Q, Asad RK. MAPE-K Interfaces for Formal Modeling of Real-Time Self-Adaptive Multi-Agent Systems. IEEE Access. 2016; 4:4946–58. CrossRef.


  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.