C. Ccspeed, F. , and ?. Bool, Cycle Length ? 500 inv3 : tic ? N inv4, 2000.

M. G. Khan, Rapid ECG Interpretation, 2008.
DOI : 10.1007/978-1-59745-408-7

W. H. Maisel, M. O. Sweeney, W. G. Stevenson, K. E. Ellison, and L. M. Epstein, Recalls and Safety Alerts Involving Pacemakers and Implantable Cardioverter-Defibrillator Generators, JAMA, vol.286, issue.7, pp.793-799, 2001.
DOI : 10.1001/jama.286.7.793

A. Reseach and . Development, Needs Report by NITRD: High-Confidence Medical Devices : Cyber-Physical Systems for 21st Century Health Care

K. L. Keatley, A REVIEW OF THE FDA DRAFT GUIDANCE DOCUMENT FOR SOFTWARE VALIDATION: GUIDANCE FOR INDUSTRY, Quality Assurance: Good Practice, Regulation, and Law, vol.7, issue.1, pp.49-55, 1999.
DOI : 10.1080/105294100277723

I. Lee, G. J. Pappas, R. Cleaveland, J. Hatcliff, B. H. Krogh et al., The Problem with Threads, Computer, vol.39, issue.5, pp.33-38, 2006.
DOI : 10.1109/MC.2006.180

D. Méry and N. K. Singh, Trustable Formal Specification for Software Certification, Lecture Notes in Computer Science, vol.6416, pp.312-326, 2010.
DOI : 10.1007/978-3-642-16561-0_31

J. Bowen and V. Stavridou, Safety-critical systems, formal methods and standards, Software Engineering Journal, vol.8, issue.4, pp.189-209, 1993.
DOI : 10.1049/sej.1993.0025
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.7190

R. P. Jetley, C. Carlos, and S. P. Iyer, A case study on applying formal methods to medical devices: computer-aided resuscitation algorithm, International Journal on Software Tools for Technology Transfer (STTT), vol.5, issue.4, pp.320-330, 2004.
DOI : 10.1007/s10009-003-0137-2

R. Jetley, P. Iyer, S. Jones, and P. , A Formal Methods Approach to Medical Device Review, Computer, vol.39, issue.4, pp.61-67, 2006.
DOI : 10.1109/MC.2006.113

D. Méry and N. K. Singh, Real-Time Animation for Formal Specification, Complex Systems Design & Management, pp.49-60, 2010.
DOI : 10.1007/978-3-642-15654-0_3

J. R. Abrial, Modeling in Event-B: System and Software Engineering, 2010.
DOI : 10.1017/CBO9781139195881

J. Fitzgerald, The Typed Logic of Partial Functions and the Vienna Development Method, pp.431-465, 2007.
DOI : 10.1007/978-3-540-74107-7_9

R. Project, Rigorous open development environment for complex systems, 2004.

D. M. Harrild, C. S. Henriquez, T. H. Atria, D. M. Harrild, and C. S. Henriquez, Cs, a computer model of normal conduction, in the Human Atria, pp.25-36, 2000.

A. Bayes-de-luna, V. N. Batcharov, M. Malik, and . In, The morphology of the Electrocardiogram " in The ESC Textbook of Cardiovascular Medicine, pp.1-36, 2006.

. John-von-neumann, Theory of Self-Reproducing Automata, 1966.

R. Plonsey and R. C. Barr, Mathematical modeling of electrical activity of the heart, Journal of Electrocardiology, vol.20, issue.3, pp.219-226, 1987.
DOI : 10.1016/S0022-0736(87)80019-5

Y. R. Kye-rok-jun and T. G. Kim, A cellular automata model of activation process in ventricular muscle

O. Berenfeld and S. Abboud, Simulation of cardiac activity and the ECG using a heart model with a reaction-diffusion action potential, Medical Engineering & Physics, vol.18, issue.8, pp.615-625, 1996.
DOI : 10.1016/S1350-4533(96)00028-8

D. Adam, Propagation of depolarization and repolarization processes in the myocardium-an anisotropic model, IEEE Transactions on Biomedical Engineering, vol.38, issue.2, pp.133-141, 1991.
DOI : 10.1109/10.76378

Z. Jiang, M. Pajic, A. T. Connolly, S. Dixit, and R. Mangharam, Real-Time Heart Model for Implantable Cardiac Device Validation and Verification, 2010 22nd Euromicro Conference on Real-Time Systems, 2010.
DOI : 10.1109/ECRTS.2010.36
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.303.8976

F. Leitner and S. Leue, Simulink Design Verifier vs. SPIN a Comparative Case Study, Proceedings of FMICS, 2008.

K. A. Ellenbogen and M. A. Wood, In: Cardiac Pacing and ICDs, Blackwell, 2005.

A. Hesselson, In: Simplified Interpretations of Pacemaker ECGs, 2003.
DOI : 10.1002/9780470695982

I. Lee, G. J. Pappas, R. Cleaveland, J. Hatcliff, B. H. Krogh et al., The Problem with Threads, Computer, vol.39, issue.5, pp.33-38, 2006.
DOI : 10.1109/MC.2006.180

C. J. Love, In: Cardiac Pacemakers and Defibrillators, 2006.

. Writing-committee-members, A. E. Epstein, J. P. Dimarco, K. A. Ellenbogen, N. A. Estes et al., ACC/AHA/HRS 2008 Guidelines for Device-Based Therapy of Cardiac Rhythm Abnormalities: Executive Summary: 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, Guidelines for Device-Based Therapy of Cardiac Rhythm Abnormalities, Developed in Collaboration With the American Association for Thoracic Surgery and Society of Thoracic Surgeons, pp.2820-2840, 2008.
DOI : 10.1161/CIRCUALTIONAHA.108.189741

D. Makowiec, The Heart Pacemaker by Cellular Automata on Complex Networks, Proceedings of the 8th international conference on Cellular Automata for Reseach and Industry. ACRI '08, pp.291-298, 2008.
DOI : 10.1007/978-3-540-79992-4_37

H. Vangheluwe and G. C. Vansteenkiste, The cellular automata formalism and its relationship to devs, Proceedings of the 14th European Simulation Multiconference on Simulation and Modelling: Enablers for a Better Quality of Life, pp.800-810, 2000.

D. Cansell and D. Méry, The event-B Modelling Method: Concepts and Case Studies, pp.33-140, 2007.
DOI : 10.1007/978-3-540-74107-7_3
URL : https://hal.archives-ouvertes.fr/inria-00579550

D. Bjorner, Software Engineering 1-2-3. Texts in Theoretical Computer Science. An EATCS Series, 2006.

D. Bjørner and M. C. Henson, Logics of Specification Languages, EATCS Textbook in Computer Science, 2007.
DOI : 10.1007/978-3-540-74107-7

G. T. Leavens, J. R. Abrial, D. Batory, M. Butler, A. Coglio et al., Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering , GPCE '06, pp.221-235, 2006.
DOI : 10.1145/1173706.1173740
URL : http://archives.cs.iastate.edu/documents/disk0/00/00/04/38/00000438-00/roadmap.pdf

E. Gamma, R. Helm, R. Johnson, R. Vlissides, and P. Gamma, Design Patterns : Elements of Reusable Object-Oriented Software design Patterns, 1994.

J. Rehm, Pattern Based Integration of Time applied to the 2-Slots Simpson Algorithm In: Integration of Model-based Formal Methods and Tools in IFM, 2009.

R. Back and J. Von-wright, Refinement Calculus A Systematic Introduction. Graduate Texts in Computer Science, 1998.

M. Leuschel, M. Butler, and . Lncs, ProB: A Model Checker for B, pp.855-874, 2003.
DOI : 10.1007/978-3-540-45236-2_46

E. M. Clarke, O. G. Peled, and D. , In: Model Checking, 1999.

D. Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology, vol.11, issue.2, pp.256-290, 2002.
DOI : 10.1145/505145.505149

D. Méry and N. K. Singh, Functional behavior of a cardiac pacing system, International Journal of Discrete Event Control Systems, vol.1, issue.2, pp.129-149, 2011.