{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T14:28:13Z","timestamp":1725805693507},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662452301"},{"type":"electronic","value":"9783662452318"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-45231-8_27","type":"book-chapter","created":{"date-parts":[[2014,9,26]],"date-time":"2014-09-26T11:42:39Z","timestamp":1411731759000},"page":"365-384","source":"Crossref","is-referenced-by-count":4,"title":["On Quantitative Software Quality Assurance Methodologies for Cardiac Pacemakers"],"prefix":"10.1007","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Paoletti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"PhysioNet, \n                    \n                      http:\/\/www.physionet.org\/physiobank\/"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"Barold, S.S., Stroobandt, R.X., Sinnaeve, A.F.: Cardiac pacemakers and resynchronization step by step: An illustrated guide. John Wiley & Sons (2010)","DOI":"10.1002\/9781444323214"},{"issue":"3","key":"27_CR3","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1016\/j.jtbi.2008.03.029","volume":"253","author":"A. Bueno-Orovio","year":"2008","unstructured":"Bueno-Orovio, A., Cherry, E.M., Fenton, F.H.: Minimal model for human ventricular action potentials in tissue. Journal of Theoretical Biology\u00a0253(3), 544\u2013560 (2008)","journal-title":"Journal of Theoretical Biology"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013272. IEEE (2012)","DOI":"10.1109\/RTSS.2012.77"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013136 (2013)","DOI":"10.1145\/2461328.2461351"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Quantitative verification of implantable cardiac pacemakers over hybrid heart models. Information and Computation (in press, 2014)","DOI":"10.1016\/j.ic.2014.01.014"},{"issue":"4","key":"27_CR7","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/2528935","volume":"14","author":"T. Chen","year":"2013","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M.Z., Mereacre, A.: Verification of linear duration properties over continuous-time markov chains. ACM Trans. Comput. Log.\u00a014(4), 33 (2013)","journal-title":"ACM Trans. Comput. Log."},{"issue":"5","key":"27_CR8","doi-asserted-by":"publisher","first-page":"595","DOI":"10.1088\/0967-3334\/31\/5\/001","volume":"31","author":"G. Clifford","year":"2010","unstructured":"Clifford, G., Nemati, S., Sameni, R.: An Artificial Vector Model for Generating Abnormal Electrocardiographic Rhythms. Physiological Measurements\u00a031(5), 595\u2013609 (2010)","journal-title":"Physiological Measurements"},{"key":"27_CR9","unstructured":"Diciolla, M.: Quantitative Verification of Real-Time Properties with Application to Medical Devices. PhD thesis, Department of Computer Science. University of Oxford (2014)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-642-05089-3_44","volume-title":"FM 2009: Formal Methods","author":"A.O. Gomes","year":"2009","unstructured":"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.\u00a05850, pp. 692\u2013707. Springer, Heidelberg (2009)"},{"issue":"9","key":"27_CR11","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/10.245605","volume":"40","author":"S. Greenhut","year":"1993","unstructured":"Greenhut, S., Jenkins, J., MacDonald, R.: A stochastic network model of the interaction between cardiac rhythm and artificial pacemaker. IEEE Transactions on Biomedical Engineering\u00a040(9), 845\u2013858 (1993)","journal-title":"IEEE Transactions on Biomedical Engineering"},{"issue":"1","key":"27_CR12","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0010-4809(89)90017-7","volume":"22","author":"F. Gritzali","year":"1989","unstructured":"Gritzali, F., Frangakis, G., Papakonstantinou, G.: Detection of the P and T waves in an ECG. Computers and Biomedical Research\u00a022(1), 83\u201391 (1989)","journal-title":"Computers and Biomedical Research"},{"key":"27_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-642-22110-1_31","volume-title":"Computer Aided Verification","author":"R. Grosu","year":"2011","unstructured":"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.\u00a06806, pp. 396\u2013411. Springer, Heidelberg (2011)"},{"key":"27_CR14","unstructured":"Guevara, M.R., Ward, G., Shrier, A., Glass, L.: Electrical alternans and period-doubling bifurcations. Computers in Cardiology, 167\u2013170 (1984)"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-319-08867-9_25","volume-title":"Computer Aided Verification","author":"Z. Huang","year":"2014","unstructured":"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.\u00a08559, pp. 373\u2013390. Springer, Heidelberg (2014)"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"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\u2013248 (2010)","DOI":"10.1109\/ECRTS.2010.36"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-28756-5_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Z. Jiang","year":"2012","unstructured":"Jiang, Z., Pajic, M., Moarref, S., Alur, R., Mangharam, R.: Modeling and verification of a dual chamber implantable pacemaker. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 188\u2013203. Springer, Heidelberg (2012)"},{"key":"27_CR18","unstructured":"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)"},{"key":"27_CR19","first-page":"4","volume":"3","author":"J. Lian","year":"2010","unstructured":"Lian, J., Kr\u00e4tschmer, H., M\u00fcssig, D., Stotts, L.: Open source modeling of heart rhythm and cardiac pacing. Open Pacing Electrophysiol. Ther. J.\u00a03, 4 (2010)","journal-title":"Open Pacing Electrophysiol. Ther. J."},{"key":"27_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1007\/BFb0020971","volume-title":"Hybrid Systems III","author":"N. Lynch","year":"1996","unstructured":"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.\u00a01066, pp. 496\u2013510. Springer, Heidelberg (1996)"},{"key":"27_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-68237-0_14","volume-title":"FM 2008: Formal Methods","author":"H.D. Macedo","year":"2008","unstructured":"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.\u00a05014, pp. 181\u2013197. Springer, Heidelberg (2008)"},{"issue":"5","key":"27_CR22","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1016\/0038-092X(93)90060-2","volume":"50","author":"J.F. Manwell","year":"1993","unstructured":"Manwell, J.F., McGowan, J.G.: Lead acid battery storage model for hybrid energy systems. Solar Energy\u00a050(5), 399\u2013405 (1993)","journal-title":"Solar Energy"},{"issue":"3","key":"27_CR23","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1109\/TBME.2003.808805","volume":"50","author":"P.E. McSharry","year":"2003","unstructured":"McSharry, P.E., Clifford, G.D., Tarassenko, L., Smith, L.A.: A dynamical model for generating synthetic electrocardiogram signals. IEEE Transactions on Biomedical Engineering\u00a050(3), 289\u2013294 (2003)","journal-title":"IEEE Transactions on Biomedical Engineering"},{"key":"27_CR24","unstructured":"M\u00e9ry, D., Singh, N.K.: Pacemaker\u2019s Functional Behaviors in Event-B. Rapport de recherche, MOSEL - INRIA Lorraine - LORIA (2009)"},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"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\u201332. IEEE (2010)","DOI":"10.1109\/SSIRI.2010.28"},{"key":"27_CR26","unstructured":"Ye, P., Entcheva, E., Grosu, R., Smolka, S.A.: Efficient modeling of excitable cells using hybrid automata. In: Proc. of CMSB, vol.\u00a05, pp. 216\u2013227 (2005)"},{"issue":"3","key":"27_CR27","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.cmpb.2008.04.006","volume":"91","author":"Y.C. Yeh","year":"2008","unstructured":"Yeh, Y.C., Wang, W.J.: QRS complexes detection for ECG signal: The Difference Operation Method. Computer Methods and Programs in Biomedicine\u00a091(3), 245\u2013254 (2008)","journal-title":"Computer Methods and Programs in Biomedicine"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-45231-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T20:19:44Z","timestamp":1558988384000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-45231-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662452301","9783662452318"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-45231-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}