The Cardiac Pacemaker

  • Neeraj Kumar Singh


Building high quality and zero defects medical software-based devices is a critical task, and formal modelling techniques can effectively help to achieve this target at the certain level. Formal modelling of a high-confidence medical device, such as that is too much error prone in operating, is an international Grand Challenge in the area of Verified Software. Modelling a cardiac pacemaker is one of the proposed challenges, and we consider the complete description of pacemaker’s functionalities using an incremental proof-based approach. To assess the effectiveness of our proposed development methodology and associated techniques and tools, we select this case study. This chapter presents the development of a cardiac pacemaker using our proposed development life-cycle methodology from requirement analysis to automatic code generation. In this development, we use formal verification to verify the correctness of the requirements for a simple and closed-loop model, model checking to verify the correctness of the system behaviours, real-time animator to check the system behaviours according to the domain experts (i.e. medical experts), and finally the code generation tool EB2ALL for generating the codes into several programming languages. The refinement charts are used to handle the complexity of the system, where it helps to organise the code structure according to the different operating modes. Formal models are expressed in the Event-B modelling language, which integrates conditions (called proof obligations) for checking their internal consistency with respect to the invariants and safety properties. The generated proof obligations of models are proved by the Rodin tool and desired behaviour of the system is validated by the ProB tool and real-time animator according to the medical experts.


Cardiac Pacemaker Heart Model Proof Obligation Impulse Propagation Refinement Level 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New York: Cambridge University Press. MATHCrossRefGoogle Scholar
  2. 2.
    Artigou, J. Y., & Monsuez, J. J. (2007). Cardiologie et maladies vasculaires. Paris: Elsevier Masson. Google Scholar
  3. 3.
    Baier, C., & Katoen, J.-P. (2008). Principles of model checking (representation and mind series). Cambridge: MIT Press. Google Scholar
  4. 4.
    Barold, S. S., Stroobandt, R. X., & Sinnaeve, A. F. (2004). Cardiac pacemakers step by step. London: Futura. ISBN 1-4051-1647-1. CrossRefGoogle Scholar
  5. 5.
    Bayes, B. V. N., de Luna, A., & Malik, M. (2006). The morphology of the electrocardiogram. In The ESC textbook of cardiovascular medicine (pp. 1–36). Oxford: Blackwell. Google Scholar
  6. 6.
    Bjørner, D., & Jones, C. B. (Eds.) (1978). The Vienna development method: The meta-language. London: Springer. MATHGoogle Scholar
  7. 7.
    Boston Scientific (2007). Pacemaker system specification (Technical report).
  8. 8.
    Cansell, D., & Méry, D. (2008). The Event-B modelling method: Concepts and case studies. In D. Bjørner & M. C. Henson (Eds.), Monographs in theoretical computer science. Logics of specification languages (pp. 47–152). Berlin: Springer. CrossRefGoogle Scholar
  9. 9.
    Cansell, D., Méry, D., & Rehm, J. (2006). Time constraint patterns for Event B development. In J. Julliand & O. Kouchnarenko (Eds.), Lecture notes in computer science: Vol. 4355. B 2007: Formal specification and development in B (pp. 140–154). Berlin: Springer. CrossRefGoogle Scholar
  10. 10.
    Clarke, E. M., Grumberg, O., & Peled, D. (2001). Model checking. Cambridge: MIT Press. Google Scholar
  11. 11.
    CC. Common criteria.
  12. 12.
    Crocker, D. (2003). Perfect developer: A tool for object-oriented formal specification and refinement. Tools exhibition notes at formal methods Europe. In Tools exhibition notes at formal methods Europe (p. 2003). Google Scholar
  13. 13.
    EB2ALL (2011). Automatic code generation from Event-B to many programming languages.
  14. 14.
    Ellenbogen, K. A., & Wood, M. A. (2005). Cardiac pacing and ICDs (4th ed.). Oxford: Blackwell. ISBN 1-4051-0447-3. CrossRefGoogle Scholar
  15. 15.
    Epstein, A. E., DiMarco, J. P., Ellenbogen, K. A., Estes, N. A. M., III, Freedman, R. A., Gettes, L. S., et al. (2008). ACC/AHA/HRS 2008 guidelines for device-based therapy of cardiac rhythm abnormalities: A report of the American College of Cardiology/American Heart Association task force on practice guidelines (writing committee to revise the ACC/AHA/NASPE 2002 guideline update for implantation of cardiac pacemakers and antiarrhythmia devices) developed in collaboration with the American Association for Thoracic Surgery and Society of Thoracic Surgeons. Journal of the American College of Cardiology, 51(21), e1–e62. CrossRefGoogle Scholar
  16. 16.
    FDA. Food and Drug Administration.
  17. 17.
    Gamma, E., Helm, R., Johnson, R., Vlissides, R., & Gamma, P. (1994). Design patterns: Elements of reusable object-oriented software design patterns. Reading: Addison-Wesley Professional. Google Scholar
  18. 18.
    Goldman, B. S., Noble, E. J., Heller, J. G., & Covvey, D. (1974). The pacemaker challenge. CMAJ. Canadian Medical Association Journal, 110(1), 28–31. Google Scholar
  19. 19.
    Gomes, A., & Oliveira, M. (2009). Formal specification of a cardiac pacing system. In A. Cavalcanti & D. Dams (Eds.), Lecture notes in computer science: Vol. 5850. FM 2009: Formal methods (pp. 692–707). Berlin: Springer. CrossRefGoogle Scholar
  20. 20.
    Gomes, A. O., & Oliveira, M. V. M. (2010). Formal development of a cardiac pacemaker: From specification to code. In Lecture notes in computer science. SBFM 2010 (pp. 213–228). Google Scholar
  21. 21.
    Harrild, D. M., & Henriquez, C. S. (2000). A computer model of normal conduction in the human atria. Circulation Research, 87, 25–36. CrossRefGoogle Scholar
  22. 22.
    Hesselson, A. (2003). Simplified interpretations of pacemaker ECGs. Oxford: Blackwell. ISBN 978-1-4051-0372-5. CrossRefGoogle Scholar
  23. 23.
    High Confidence Software and Systems Coordinating Group (2009). High-confidence medical devices: Cyber-physical systems for 21st century health care (Technical report). NITRD.
  24. 24.
    Hoare, C. A. R. (2003). The verifying compiler: A grand challenge for computing research. In H. Kosch, L. Böszörményi, & H. Hellwagner (Eds.), Lecture notes in computer science: Vol. 2790. Euro-Par 2003 parallel processing (p. 1). Berlin: Springer. CrossRefGoogle Scholar
  25. 25.
    Hoare, C. A. R., Misra, J., Leavens, G. T., & Shankar, N. (2009). The verified software initiative: A manifesto. ACM Computing Surveys, 41(4), 22:1–22:8. Google Scholar
  26. 26.
    IEEE-SA. IEEE Standards Association.
  27. 27.
    ISO. International Organization for Standardization.
  28. 28.
    Jackson, D. (2002). Alloy: A lightweight object modelling notation. ACM Transactions on Software Engineering and Methodology, 11(2), 256–290. CrossRefGoogle Scholar
  29. 29.
    Jiang, Z., Pajic, M., & Mangharam, R. (2011). Model-based closed-loop testing of implantable pacemakers. In 2011 IEEE/ACM international conference on cyber-physical systems, ICCPS (pp. 131–140). CrossRefGoogle Scholar
  30. 30.
    Jiang, Z., Pajic, M., Moarref, S., Alur, R., & Mangharam, R. (2012). Modeling and verification of a dual chamber implantable pacemaker. In C. Flanagan & B. König (Eds.), Lecture notes in computer science: Vol. 7214. Tools and algorithms for the construction and analysis of systems (pp. 188–203). Berlin: Springer. CrossRefGoogle Scholar
  31. 31.
    Kantharia, B. K., & Kutalek, S. P. (1999). Optimal programming of rate modulation functions. Cardiac Electrophysiology Review, 3, 53–55. doi: 10.1023/A:1009935600754. CrossRefGoogle Scholar
  32. 32.
    Keatley, K. L. (1999). A review of the FDA draft guidance document for software validation: Guidance for industry. Quality Assurance, 7(1), 49–55. Google Scholar
  33. 33.
    Khan, M. G. (2008). Rapid ECG interpretation. Clifton: Humana Press. CrossRefGoogle Scholar
  34. 34.
    La Manna, V. P., Bonanno, A. T., & Motta, A. (2009). Poster on a simple pacemaker implementation. New York: ACM. Google Scholar
  35. 35.
    Lee, I., Pappas, G. J., Cleaveland, R., Hatcliff, J., Krogh, B. H., Lee, P., et al. (2006). High-confidence medical device software and systems. Computer, 39(4), 33–38. CrossRefGoogle Scholar
  36. 36.
    Leuschel, M., & Butler, M. (2003). Lecture notes in computer science. ProB: A model checker for B (pp. 855–874). Berlin: Springer. Google Scholar
  37. 37.
    Love, C. J. (2006). Cardiac pacemakers and defibrillators. Georgetown: Landes Bioscience. ISBN 1-57059-691-3. Google Scholar
  38. 38.
    Macedo, H. D., Larsen, P. G., & Fitzgerald, J. (2008). Incremental development of a distributed real-time model of a cardiac pacing system using VDM. In Lecture notes in computer science. Proceedings of the 15th international symposium on formal methods, FM’08 (pp. 181–197). Berlin: Springer. Google Scholar
  39. 39.
    Malmivuo, J. (1995). Bioelectromagnetism. Oxford: Oxford University Press. ISBN 0-19-505823-2. Google Scholar
  40. 40.
    Méry, D., & Singh, N. K. (2009). Pacemaker’s functional behaviors in Event-B (Research report). MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-Nancy I-Université Nancy II-Institut National Polytechnique de Lorraine.
  41. 41.
    Méry, D., & Singh, N. K. (2010). EB2C: A tool for Event-B to C conversion support. Poster and tool demo submission, published in a CNR technical report in SEFM. Google Scholar
  42. 42.
    Méry, D., & Singh, N. K. (2010). Real-time animation for formal specification. In M. Aiguier, F. Bretaudeau, & D. Krob (Eds.), Complex systems design & management (pp. 49–60). Berlin: Springer. CrossRefGoogle Scholar
  43. 43.
    Méry, D., & Singh, N. K. (2010). Technical report on formal development of two-electrode cardiac pacing system. MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-Nancy I-Université Nancy II-Institut National Polytechnique de Lorraine.
  44. 44.
    Méry, D., & Singh, N. K. (2010). Trustable formal specification for software certification. In T. Margaria & B. Steffen (Eds.), Lecture notes in computer science: Vol. 6416. Leveraging applications of formal methods, verification, and validation (pp. 312–326). Berlin: Springer. CrossRefGoogle Scholar
  45. 45.
    Méry, D., & Singh, N. (2011). A generic framework: From modeling to code. In Innovations in systems and software engineering (pp. 1–9). Google Scholar
  46. 46.
    Méry, D., & Singh, N. K. (2011). Automatic code generation from Event-B models. In Proceedings of the second symposium on information and communication technology, SoICT’11 (pp. 179–188). New York: ACM. CrossRefGoogle Scholar
  47. 47.
    Méry, D., & Singh, N. K. (2011). EB2J: Code generation from Event-B to Java. Short paper presented at the 14th Brazilian symposium on formal methods, SBMF’11. Google Scholar
  48. 48.
    Méry, D., & Singh, N. K. (2011). Functional behavior of a cardiac pacing system. International Journal of Discrete Event Control Systems, 1(2), 129–149. Google Scholar
  49. 49.
    Méry, D., & Singh, N. K. (2011). Technical report on formalisation of the heart using analysis of conduction time and velocity of the electrocardiography and cellular-automata. MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-Nancy I-Université Nancy II-Institut National Polytechnique de Lorraine.
  50. 50.
    Méry, D., & Singh, N. K. (2012). Closed-loop modeling of cardiac pacemaker and heart. In Foundations of health informatics engineering and systems. Google Scholar
  51. 51.
    Méry, D., & Singh, N. K. (2012). Formal development and automatic code generation: Cardiac pacemaker. New York: ASME Press. Google Scholar
  52. 52.
    Méry, D., & Singh, N. K. (2012). Formalization of heart models based on the conduction of electrical impulses and cellular automata. In Z. Liu & A. Wassyng (Eds.), Lecture notes in computer science: Vol. 7151. Foundations of health informatics engineering and systems (pp. 140–159). Berlin: Springer. CrossRefGoogle Scholar
  53. 53.
    Méry, D., & Singh, N. K. (2013). Formal specification of medical systems by proof-based refinement. ACM Transactions on Embedded Computing Systems, 12(1), 15:1–15:25. CrossRefGoogle Scholar
  54. 54.
    MIT-BIH. MIT-BIH database distribution and software.
  55. 55.
    Rehm, J. (2010). Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the Event-B method. International Journal on Software Tools for Technology Transfer, 12(1), 39–51. CrossRefGoogle Scholar
  56. 56.
    RODIN (2004). Rigorous open development environment for complex systems.
  57. 57.
    Singh, N. K., Wellings, A., & Cavalcanti, A. (2012). The cardiac pacemaker case study and its implementation in safety-critical Java and Ravenscar Ada. In Proceedings of the 10th international workshop on Java technologies for real-time and embedded systems, JTRES’12 (pp. 62–71). New York: ACM. CrossRefGoogle Scholar
  58. 58.
    Tuan, L. A., Zheng, M. C., & Tho, Q. T. (2010). Modeling and verification of safety critical systems: A case study on pacemaker. In Secure system integration and reliability improvement (pp. 23–32). Google Scholar
  59. 59.
    Woodcock, J. (2006). First steps in the verified software grand challenge. Computer, 39(10), 57–64. CrossRefGoogle Scholar
  60. 60.
    Woodcock, J., & Banach, R. (2007). The verification grand challenge. Journal of Universal Computer Science, 13(5), 661–668. Google Scholar

Copyright information

© Springer-Verlag London 2013

Authors and Affiliations

  • Neeraj Kumar Singh
    • 1
  1. 1.Department of Computing and SoftwareMcMaster UniversityHamiltonCanada

Personalised recommendations