Skip to main content
SpringerLink
Log in

On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers

  • Conference paper
Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications (ISoLA 2014)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8803))

Abstract

Embedded software is at the heart of implantable medical devices such as cardiac pacemakers, and rigorous software design methodologies are needed to ensure their safety and reliability. This paper gives an overview of ongoing research aimed at providing software quality assurance methodologies for pacemakers. A model-based framework has been developed based on hybrid automata, which can be configured with a variety of heart and pacemaker models. The framework supports a range of quantitative verification techniques for the analysis of safety, reliability and energy usage of pacemakers. It also provides techniques for parametric analysis of personalised physiological properties that can be performed in silico, which can reduce the cost and discomfort of testing new designs on patients. We describe the framework, summarise the results obtained, and identify future research directions in this area.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. PhysioNet, http://www.physionet.org/physiobank/

  2. Barold, S.S., Stroobandt, R.X., Sinnaeve, A.F.: Cardiac pacemakers and resynchronization step by step: An illustrated guide. John Wiley & Sons (2010)

    Google Scholar 

  3. Bueno-Orovio, A., Cherry, E.M., Fenton, F.H.: Minimal model for human ventricular action potentials in tissue. Journal of Theoretical Biology 253(3), 544–560 (2008)

    Article  MathSciNet  Google Scholar 

  4. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers. In: 2012 IEEE 33rd Real-Time Systems Symposium (RTSS), pp. 263–272. IEEE (2012)

    Google Scholar 

  5. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: A simulink hybrid heart model for quantitative verification of cardiac pacemakers. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pp. 131–136 (2013)

    Google Scholar 

  6. Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation (in press, 2014)

    Google Scholar 

  7. Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: Verification of linear duration properties over continuous-time markov chains. ACM Trans. Comput. Log. 14(4), 33 (2013)

    Article  MathSciNet  Google Scholar 

  8. Clifford, G., Nemati, S., Sameni, R.: An Artificial Vector Model for Generating Abnormal Electrocardiographic Rhythms. Physiological Measurements 31(5), 595–609 (2010)

    Article  Google Scholar 

  9. Diciolla, M.: Quantitative Verification of Real-Time Properties with Application to Medical Devices. PhD thesis, Department of Computer Science. University of Oxford (2014)

    Google Scholar 

  10. Gomes, A.O., Oliveira, M.V.M.: Formal specification of a cardiac pacing system. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 692–707. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  11. Greenhut, S., Jenkins, J., MacDonald, R.: A stochastic network model of the interaction between cardiac rhythm and artificial pacemaker. IEEE Transactions on Biomedical Engineering 40(9), 845–858 (1993)

    Article  Google Scholar 

  12. Gritzali, F., Frangakis, G., Papakonstantinou, G.: Detection of the P and T waves in an ECG. Computers and Biomedical Research 22(1), 83–91 (1989)

    Article  Google Scholar 

  13. Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Guevara, M.R., Ward, G., Shrier, A., Glass, L.: Electrical alternans and period-doubling bifurcations. Computers in Cardiology, 167–170 (1984)

    Google Scholar 

  15. Huang, Z., Fan, C., Mereacre, A., Mitra, S., Kwiatkowska, M.: Invariant verification of nonlinear hybrid automata networks of cardiac cells. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 373–390. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  16. Jiang, Z., Pajic, M., Connolly, A., Dixit, S., Mangharam, R.: Real-time heart model for implantable cardiac device validation and verification. In: ECRTS, pp. 239–248 (2010)

    Google Scholar 

  17. Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 188–203. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  18. Kwiatkowska, M., Lea-Banks, H., Mereacre, A., Paoletti, N.: Formal modelling and validation of rate-adaptive pacemakers. In: IEEE International Conference on Healthcare Informatics 2014, ICHI 2014 (to appear, 2014)

    Google Scholar 

  19. Lian, J., Krätschmer, H., Müssig, D., Stotts, L.: Open source modeling of heart rhythm and cardiac pacing. Open Pacing Electrophysiol. Ther. J. 3, 4 (2010)

    Google Scholar 

  20. Lynch, N., Segala, R., Vaandrager, F., Weinberg, H.B.: Hybrid I/O automata. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 496–510. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  21. Macedo, H.D., Larsen, P.G., Fitzgerald, J.: Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 181–197. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  22. Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Solar Energy 50(5), 399–405 (1993)

    Article  Google Scholar 

  23. McSharry, P.E., Clifford, G.D., Tarassenko, L., Smith, L.A.: A dynamical model for generating synthetic electrocardiogram signals. IEEE Transactions on Biomedical Engineering 50(3), 289–294 (2003)

    Article  Google Scholar 

  24. Méry, D., Singh, N.K.: Pacemaker’s Functional Behaviors in Event-B. Rapport de recherche, MOSEL - INRIA Lorraine - LORIA (2009)

    Google Scholar 

  25. Tuan, L.A., Zheng, M.C., Tho, Q.T.: Modeling and verification of safety critical systems: A case study on pacemaker. In: 2010 Fourth International Conference on Secure Software Integration and Reliability Improvement (SSIRI), pp. 23–32. IEEE (2010)

    Google Scholar 

  26. Ye, P., Entcheva, E., Grosu, R., Smolka, S.A.: Efficient modeling of excitable cells using hybrid automata. In: Proc. of CMSB, vol. 5, pp. 216–227 (2005)

    Google Scholar 

  27. Yeh, Y.C., Wang, W.J.: QRS complexes detection for ECG signal: The Difference Operation Method. Computer Methods and Programs in Biomedicine 91(3), 245–254 (2008)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, UK

    Marta Kwiatkowska, Alexandru Mereacre & Nicola Paoletti

Authors
  1. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexandru Mereacre
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicola Paoletti
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kwiatkowska, M., Mereacre, A., Paoletti, N. (2014). On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications. ISoLA 2014. Lecture Notes in Computer Science, vol 8803. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45231-8_27

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-45231-8_27

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-45230-1

  • Online ISBN: 978-3-662-45231-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation