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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
PhysioNet, http://www.physionet.org/physiobank/
Barold, S.S., Stroobandt, R.X., Sinnaeve, A.F.: Cardiac pacemakers and resynchronization step by step: An illustrated guide. John Wiley & Sons (2010)
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)
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)
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)
Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation (in press, 2014)
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)
Clifford, G., Nemati, S., Sameni, R.: An Artificial Vector Model for Generating Abnormal Electrocardiographic Rhythms. Physiological Measurements 31(5), 595–609 (2010)
Diciolla, M.: Quantitative Verification of Real-Time Properties with Application to Medical Devices. PhD thesis, Department of Computer Science. University of Oxford (2014)
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)
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)
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)
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)
Guevara, M.R., Ward, G., Shrier, A., Glass, L.: Electrical alternans and period-doubling bifurcations. Computers in Cardiology, 167–170 (1984)
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)
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)
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)
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)
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)
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)
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)
Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Solar Energy 50(5), 399–405 (1993)
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)
Méry, D., Singh, N.K.: Pacemaker’s Functional Behaviors in Event-B. Rapport de recherche, MOSEL - INRIA Lorraine - LORIA (2009)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)