M. Ábrahám-mummmumm, U. Steffen, and . Hannemann, Verification of Hybrid Systems: Formalization and Proof Rules in PVS, International Conference on Engineering of Complex Computer Systems (ICECCS), pp.48-57, 2001.

]. Abrial-1996a and . Abrial, The B book -Assigning Programs to Meanings, pp.98-117, 1996.

]. Abrial, Extending B without changing it (for developing distributed systems), st Conference on the B method, pp.169-190, 1996.

]. Abrial, B#: Toward a Synthesis between Z and B, 3nd International Conference of B and Z Users -ZB 2003, p.50, 2003.
DOI : 10.1007/3-540-44880-2_12

]. Abrial, D. Cansell, and D. Méry, A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol, Formal Aspects of Computing, vol.14, issue.3, pp.215-227, 2003.
DOI : 10.1007/s001650300002

URL : https://hal.archives-ouvertes.fr/inria-00099531

]. Abrial, Modeling in Event-B: System and Software Engineering, pp.141-162, 2010.
DOI : 10.1017/CBO9781139195881

]. S. Acuña and N. Juristo, Software process modeling. International series in software engineering, pp.35-65, 2005.

]. 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

A. Advani, M. Goldstein, Y. Shahar, A. Mark, and . Musen, Developing Quality Indicators and Auditing Protocols from Formal Guideline Models: Knowledge Representation and Transformations, AMIA Annual Symposium proceedings AMIA Symposium AMIA Symposium, pp.11-15, 2003.

B. T. Aizenbud-reshef, J. Nolan, Y. Rubin, and . Shaham-gafni, Model traceability, IBM Systems Journal, vol.45, issue.3, pp.515-526, 2006.
DOI : 10.1147/sj.453.0515

]. Arnold, J. Gosling, and D. Holmes, The java programming language, 2005.

]. J. Artigou, J. J. Société-française-de-cardiologie, and . Monsuez, Cardiologie et maladies vasculaires, pp.47-130, 2007.

]. R. Back, On correct refinement of programs, Journal of Computer and System Sciences, vol.23, issue.1, pp.49-68, 1979.
DOI : 10.1016/0022-0000(81)90005-2

]. R. Back, A calculus of refinements for program derivations, Acta Informatica, vol.14, issue.3, pp.593-624, 1998.
DOI : 10.1145/362575.362577

]. R. Back and J. Wright, Refinement Calculus A Systematic Introduction. Graduate Texts in Computer Science, 1998.

F. Badeau and A. Amelot, Using B as a High Level Programming Language in an Industrial Project: Roissy VAL, ZB 2005: Formal Specification and Development in Z and B, pp.15-25, 2005.
DOI : 10.1007/11415787_20

J. Katoen, Principles of Model Checking (Representation and Mind Series), 2008.

M. Balser, W. Reif, G. Schellhorn, and K. Stenzel, KIV 3.0 for Provably Correct Systems, Lecture Notes in Computer Science, vol.1641, pp.330-337, 1999.
DOI : 10.1007/3-540-48257-1_23

M. Robert, N. M. Balzer, D. S. Goldman, and . Wile, Operational specification as the basis for rapid prototyping, SIGSOFT Softw. Eng. Notes, vol.7, pp.3-16, 1982.

]. S. Barold and R. X. , Stroobandt and Alfons F. Sinnaeve. Cardiac pacemakers step by step, pp.131-254, 2004.

R. Victor, A. J. Basili, and . Turner, Iterative enhancement: A practical technique for software development, IEEE Transactions on Software Engineering, vol.4, pp.390-396, 1975.

S. Bäumler, M. Balser, A. Dunets, W. Reif, and J. Schmitt, Verification of Medical Guidelines by Model Checking ??? A Case Study, Model Checking Software, pp.219-233, 2006.
DOI : 10.1007/s100090050010

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

]. P. Behm, P. Benoit, A. Faivre, and J. Meynadier, M??t??or: A Successful Application of B in a Large Project, Proceedings of FM'99: World Congress on Formal Methods, pp.369-387, 1999.
DOI : 10.1007/3-540-48119-2_22

]. R. Bell and D. Reinert, Risk and system integrity concepts for safety-related control systems, Microprocessors and Microsystems, vol.17, issue.1, pp.3-15, 1993.
DOI : 10.1016/0141-9331(93)90088-O

]. Bengtsson, K. Larsen, F. Larsson, P. Pettersson, and W. Yi, UPPAAL -a Tool Suite for Automatic Verification of Real-Time Systems, 1996.

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

M. Bernardo, R. Cleaveland, S. Sims, and W. Stewart, Twotowers: A Tool Integrating Functional and Performance Analysis of Concurrent Systems, Proceedings of the FIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV Bibliography XVIII), FORTE XI / PSTV XVIII '98, pp.457-467, 1998.
DOI : 10.1007/978-0-387-35394-4_28

M. Bernardo and E. Bonta, Generating well-synchronized multithreaded programs from software architecture descriptions, Proceedings. Fourth Working IEEE/IFIP Conference on Software Architecture (WICSA 2004), pp.167-176, 2004.
DOI : 10.1109/WICSA.2004.1310700

]. Berry, A. Bouali, X. Fornari, E. Ledinot, E. Nassor et al., ESTEREL: a formal method applied to avionic software development, Science of Computer Programming, vol.36, issue.1, pp.5-25, 2000.
DOI : 10.1016/S0167-6423(99)00015-5

URL : https://hal.archives-ouvertes.fr/hal-00579632

D. Bert, S. Boulmé, M. Potet, A. Requet, and L. Voisin, Adaptable Translator of B Specifications to Embedded C Programs, International Symposium of Formal Methods Europe, pp.94-113, 2003.
DOI : 10.1007/978-3-540-45236-2_7

A. Bertolino and L. Strigini, Acceptance Criteria for Critical Software Based on Testability Estimates and Test Results, SAFECOMP 96, Proc. of the 15th International Conference on Computer Safety, Reliability and Security, pp.83-94, 1997.
DOI : 10.1007/978-1-4471-0937-2_7

]. V. Berzins, A. Luqi, and . Yehudai, Using transformations in specificationbased prototyping. Software Engineering, IEEE Transactions on, vol.19, issue.5, pp.436-452, 1993.

]. Beyer, T. Henzinger, R. Jhala, and R. Majumdar, The software model checker Blast, International Journal on Software Tools for Technology Transfer, vol.2, issue.4, pp.505-525, 2007.
DOI : 10.1007/978-1-4757-3540-6

F. Blaauboer, K. Sikkel, and M. N. Aydin, Deciding to Adopt Requirements Traceability in Practice, Proceedings of the 19th international conference on Advanced information systems engineering, CAiSE'07, pp.294-308, 2007.
DOI : 10.1007/978-3-540-72988-4_21

N. Blanc, A. Groce, and D. Kroening, Verifying C++ with STL containers via predicate abstraction, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering , ASE '07, pp.521-524, 2007.
DOI : 10.1145/1321631.1321724

URL : http://www-2.cs.cmu.edu/~agroce/ase07.pdf

]. B. Blanchard and W. J. Fabrycky, Systems engineering and analysis. Prentice-Hall international series in industrial and systems engineering, 2006.

]. Bloomfield and P. Froo, The application of formal methods to the assessment of high integrity software, IEEE Transactions on Software Engineering, vol.12, issue.9, pp.988-993, 1986.
DOI : 10.1109/TSE.1986.6313053

]. B. Boehm, Software Engineering, IEEE Transactions on Computers, vol.25, issue.12, pp.1226-1241, 1976.
DOI : 10.1109/TC.1976.1674590

W. Barry and . Boehm, Software Engineering Economics, 1981.

]. E. Bonta and M. Bernardo, PADL2Java: A Java code generator for process algebraic architectural descriptions, 2009 Joint Working IEEE/IFIP Conference on Software Architecture & European Conference on Software Architecture, pp.161-170, 2009.
DOI : 10.1109/WICSA.2009.5290802

]. E. Börger and R. Stärk, The Abstract State Machines Method for High-Level System Design and Analysis, 2003.
DOI : 10.1007/978-1-84882-736-3_3

A. Bottrighi, L. Giordano, G. Molino, S. Montani, P. Terenziani et al., Adopting model checking techniques for clinical guidelines verification, Artificial Intelligence in Medicine, vol.48, issue.1, pp.1-19, 2010.
DOI : 10.1016/j.artmed.2009.09.003

]. 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

]. J. Britt, Case study: Applying formal methods to the Traffic Alert and Collision Avoidance System (TCAS) II. In Computer Assurance, 1994. COMPASS '94 Safety, Reliability, Fault Tolerance, Concurrency and Real Time, Security, Proceedings of the Ninth Annual Conference on, pp.39-51, 1994.

. Jr and J. A. Bubenko, Challenges in requirements engineering, Requirements Engineering Proceedings of the Second IEEE International Symposium on, pp.160-162, 1995.

A. Burns, B. Dobbing, and T. Vardanega, Guide for the use of the Ada Ravenscar Profile in high integrity systems, ACM SIGAda Ada Letters, vol.XXIV, issue.2, pp.1-74, 2004.
DOI : 10.1145/997119.997120

]. M. Butler, Stepwise refinement of communicating systems, Science of Computer Programming, vol.27, issue.2, pp.139-173, 1996.
DOI : 10.1016/0167-6423(96)81173-7

W. Ricky and . Butler, An Introduction to Requirements Capture Using PVS: Specification of a Simple Autopilot, p.64, 1996.

D. Cansell, G. Gopalakrishnan, M. Jones, D. Méry, and A. Weinzoepflen, Incremental Proof of the Producer/Consumer Property for the PCI Protocol, Proceedings of the 2nd International Conference of B and Z Users on Formal Specification and Development in Z and B, ZB '02, pp.22-41, 2002.
DOI : 10.1007/3-540-45648-1_2

URL : https://hal.archives-ouvertes.fr/inria-00100888

]. K. Chandy and J. Misra, Parallel program design a foundation, 1988.

J. M. Wing, Formal Methods: State of the Art and Future Directions, ACM Computing Surveys, vol.28, issue.40, pp.626-643, 1996.
URL : https://hal.archives-ouvertes.fr/hal-00444076

]. E. Clarke, O. Grumberg, and D. Peled, Model checking, pp.68-239, 0200.

]. E. Clarke, O. Grumberg, and D. A. Peled, Model checking, 2000.

]. W. Clocksin and C. S. Mellish, Programming in prolog, 1987.

]. D. Coleman and J. W. Hughes, The clean termination of Pascal programs, Acta Informatica, vol.2, issue.3, pp.195-210, 1979.
DOI : 10.1007/978-1-4615-9984-5

R. Patrick-cousot, J. Cousot, L. Feret, A. Mauborgne, D. Miné et al., Combination of abstractions in the ASTRÉE static analyzer, Proceedings of the 11th Asian computing science conference on Advances in computer science: secure software and related issues, pp.272-300, 2007.

J. Crow, S. Owre, and J. Rushby, Natarajan Shankar and Ayam Srivas. A Tutorial Introduction to PVS, pp.41-44, 1995.

]. W. Cullyer, Implementing high integrity systems: the VIPER microprocessor Aerospace and Electronic Systems Magazine, IEEE, vol.4, issue.6, pp.5-13, 1989.

]. W. Cullyer, S. J. Goodenough, and B. A. Wichmann, The choice of computer languages for use in safety-critical systems, Software Engineering Journal, vol.6, issue.2, pp.51-58, 1991.
DOI : 10.1049/sej.1991.0007

A. M. Davis, Operational prototyping: a new development approach, IEEE Software, vol.9, issue.5, pp.70-78, 1992.
DOI : 10.1109/52.156899

F. Dorticós, M. A. Quiones, F. Tornes, Y. Fayad, R. Zayas et al., Rate-Responsive Pacing Controlled by the TVI Sensor in the Treatment of Sick Sinus Syndrome, pp.581-590, 2005.
DOI : 10.1007/88-470-0371-7_71

F. Dotti, A. Iliasov, L. Ribeiro, and A. Romanovsky, Modal Systems: Specification, Refinement and Realisation, Formal Methods and Software Engineering, pp.601-619, 2009.
DOI : 10.1007/978-3-642-10373-5_31

]. D. Duce, Formal Methods and Standards -An Idiosyncratic View, 2nd BCS-FACS Northern Formal Methods Workshop, 1997.

A. Kenneth, M. A. Ellenbogen, and . Wood, Cardiac Pacing and ICDs, pp.131-255, 2005.

S. Kwo-jean-farn, A. Lin, and . Fung, A study on information security management system evaluation???assets, threat and vulnerability, Computer Standards & Interfaces, vol.26, issue.6, pp.501-513, 2004.
DOI : 10.1016/j.csi.2004.03.012

. Fda and . Fda, Food and Drug Administration, www.fda.gov, pp.65-207

S. John, J. W. Fitzgerald, D. Bryans, . Greathead, B. Clifff et al., Animation-based validation of a formal model of dynamic virtual organisations. Electronic Workshops in Computing, 2008.

G. Fohler, Realizing Changes of Operational Modes with a Pre Run-Time Scheduled Hard Real-Time System, Proceedings of the Second International Workshop on Responsive Computer Systems, pp.287-300, 1992.
DOI : 10.1007/978-3-7091-9288-7_16

C. Higgins, J. Mcdermid, J. Forder, and G. Storrs, SAM-A Tool to Support the Construction, Review and Evolution of Safety Arguments, Directions in Safety-Critical Systems, pp.195-216, 1993.

]. Fox, N. Johns, and A. Rahmanzadeh, Disseminating medical knowledge: the PROforma approach, Artificial Intelligence in Medicine, vol.14, issue.1-2, pp.157-182, 1998.
DOI : 10.1016/S0933-3657(98)00021-9

]. N. Fuchs, Specifications are (preferably) executable, Software Engineering Journal, vol.7, issue.5, pp.323-334, 1992.
DOI : 10.1049/sej.1992.0033

H. Gall, Functional safety IEC 61508 / IEC 61511 the impact to certification and the user, 2008 IEEE/ACS International Conference on Computer Systems and Applications, pp.1027-1031, 2008.
DOI : 10.1109/AICCSA.2008.4493673

A. Goknil, Survey of Traceability Approaches in Model-Driven Engineering, Proceedings of the 11th IEEE International Enterprise Distributed Object Computing Conference, p.313, 2007.

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

]. Georg, J. Bieman, and R. B. France, Using Alloy and UM- L/OCL to Specify Run-Time Configuration Management: A Case Study, Practical UML-Based Rigorous Development Methods -Countering or Integrating the eXtremists, pp.128-141, 2001.

W. Wayt and . Gibbs, Software's Chronic Crisis. Scientific American, 1994.

]. Goguen and J. Meseguer, Rapid prototyping, ACM SIGSOFT Software Engineering Notes, vol.7, issue.5, pp.75-84, 1982.
DOI : 10.1145/1006258.1006273

]. B. Goldman, E. J. Noble, J. G. Heller, and D. Covvey, The Pacemaker Challenge, CMAJ, vol.110, issue.162, pp.28-31, 1974.

A. Gomes and M. Oliveira, Formal Specification of a Cardiac Pacing System, Lecture Notes in Computer Science, vol.5850, issue.164, pp.692-707, 2009.
DOI : 10.1007/978-3-642-05089-3_44

A. Oliveira, G. , and M. Oliveira, Formal Development of a Cardiac Pacemaker: from Specification to Code, SBFM 2010, pp.213-228, 2010.

]. M. Gordon, LCF-LSM: a system for specifying and verifying hardware, 1983.

C. Z. Orlena, A. C. Gotel, and . Finkelstein, An Analysis of the Requirements Traceability Problem, pp.94-101, 1994.

Y. , Y. Wang, P. Yang, and F. Li, An Ontology Based Improved Software Requirement Traceability Matrix, Proceedings of the 2009 Second International Symposium on Knowledge Acquisition and Modeling, pp.160-163, 2009.

]. N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud, The synchronous dataflow programming language LUSTRE, Proceedings of the IEEE, pp.1305-1320, 1991.

]. Harel, Algorithmics: the spirit of computing, 1987.
DOI : 10.1007/978-3-642-27266-0

]. Harel, Statecharts: a visual formalism for complex systems, Science of Computer Programming, vol.8, issue.3, pp.231-274, 1987.
DOI : 10.1016/0167-6423(87)90035-9

M. David, C. S. Harrild, . Henriquez, D. M. The-human-atria, C. S. Harrild et al., A Computer Model of Normal Conduction in the Human Atria, the Human Atria, pp.25-36, 2000.
DOI : 10.1161/01.RES.87.7.e25

I. Hayes and C. B. Jones, Specifications are not (necessarily) executable, Software Engineering Journal, vol.4, issue.6, pp.330-338, 1989.
DOI : 10.1049/sej.1989.0045

P. E. Mats, N. G. Heimdahl, and . Leveson, Completeness and Consistency in Hierarchical State-Based Requirements, IEEE Trans. Softw. Eng, vol.22, pp.363-377, 1996.

L. Constance, M. Heitmeyer, E. I. Archer, J. Leonard, and . Mclean, Applying Formal Methods to a Certifiably Secure Software System, IEEE Trans. Software Eng, vol.34, issue.1, pp.82-98, 2008.

L. Constance and . Heitmeyer, On the Role of Formal Methods in Software Certification: An Experience Report, Electr. Notes Theor. Comput. Sci, vol.238, issue.4, pp.3-9, 2009.

. Henderson and . Henderson, Functional programming, formal specification, and rapid prototyping, IEEE Transactions on Software Engineering, vol.12, issue.2, pp.241-250, 1986.
DOI : 10.1109/TSE.1986.6312939

]. P. Henderson and C. J. Minkowitz, The me too Method of Software Design, ICL Journal, vol.5, issue.1, 1986.

]. C. Hennebert and G. Guiho, SACEM: A fault tolerant system for train speed control FTCS-23. Digest of Papers, Fault-Tolerant Computing The Twenty-Third International Symposium on, pp.624-628, 1993.

C. Martin, M. Henson, S. Deutsch, and . Reeves, Z logic and its applications, pp.467-569, 2007.

]. M. Hinchey and J. P. Bowen, Applications of formal methods. Prentice- Hall international series in computer science, 1995.

]. J. Hoare-1996, J. Hoare, D. Dick, I. Neilson, and . Holm-sørensen, Applying the B technologies to CICS, FME 96, pp.74-84, 1996.
DOI : 10.1007/3-540-60973-3_81

T. Hoare and . Hoare, The verifying compiler: A grand challenge for computing research, Journal of the ACM, vol.50, issue.1, pp.63-69, 2003.
DOI : 10.1145/602382.602403

]. C. Hoare-2009, J. Hoare, G. T. Misra, N. Leavens, and . Shankar, The verified software initiative, ACM Computing Surveys, vol.41, issue.4, pp.1-8, 2009.
DOI : 10.1145/1592434.1592439

J. Gerard and . Holzmann, The Model Checker SPIN, IEEE Trans. Softw. Eng, vol.23, pp.279-295, 1997.

]. W. Hosier, Pitfalls and Safeguards in Real-Time Digital Systems with Emphasis on Programming. Engineering Management, IRE Transactions on, vol.8, issue.2, pp.99-115, 1961.

H. Amy, Concept of Operations and Voluntary Operational Requirements for Forward Collision Warning Systems (CWS) and Adaptive Cruise Control (ACC) Systems On-board Commercial Motor Vehicles. FMCSA, Federal Motor Carrier Safety Administration Office of Research and Analysis, p.225, 2005.

I. Houston and S. King, CICS project report experiences and results from the use of Z in IBM, VDM'91 Formal Software Development Methods, pp.588-596, 1991.
DOI : 10.1007/3-540-54834-3_34

]. D. Hrovat and W. J. Johnson, Automotive control systems: past, present, future, Proceedings IECON '91: 1991 International Conference on Industrial Electronics, Control and Instrumentation, p.216, 1991.
DOI : 10.1109/IECON.1991.239321

M. Huhn and A. Zechner, Arguing for Software Quality in an IEC 62304 Compliant Development Process, Leveraging Applications of Formal Methods, Verification, and Validation, pp.296-311, 2010.
DOI : 10.1109/MC.2008.37

]. M. Elizabeth, K. Hull, J. Jackson, and . Dick, Requirements engineering , second edition, 2005.

I. Std, 1012-1998 ] IEEE Std. 1012-1998. IEEE Standard for Software Verification and Validation

. Std, 1074-1997 ] IEEE Std. 1074-1997. IEEE Standard for Developing Software Life Cycle Processes, p.293

. Std, 730-1998 ] IEEE Std. 730-1998, IEEE Standard for Software Quality Assurance Plans

A. David-isern and . Moreno, Computer-based execution of clinical guidelines: A review, International Journal of Medical Informatics, vol.77, issue.12, pp.787-808, 2008.
DOI : 10.1016/j.ijmedinf.2008.05.010

. Iso and . Iso, International Organization for Standardization, pp.72-281

A. K. Mok, Modechart: A Specification Language for Real-Time Systems, IEEE Trans. Softw. Eng, vol.20, issue.12, pp.933-947, 1994.

S. Jee-2010-]-eunkyoung-jee, J. Wang, J. Kim, O. Lee, I. Sokolsky et al., A Safety-Assured Development Approach for Real-Time Software, 16th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, RTCSA, pp.133-142, 2010.

R. Praful-jetley, C. Carlos, and S. 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, S. Iyer, and P. Jones, A Formal Methods Approach to Medical Device Review, Computer, vol.39, issue.4, pp.61-67, 2006.
DOI : 10.1109/MC.2006.113

Z. Jiang, M. Pajic, and A. T. Connolly, Sanjay Dixit and Rahul Mangharam. Real-time Heart Model for Implantable Cardiac Device Validation and Verification, 22st Euromicro Conference on Real-Time Systems, p.7, 2010.

]. C. Jones, Systematic software development using vdm, 1986.

B. Clifford and . Jones, Systematic Software Development using VDM. Prentice Hall International Series in Computer Science, pp.43-44, 1986.

R. Kaivola, R. Ghughal, N. Narasimhan, A. Telfer, J. Whittemore et al., Replacing Testing with Formal Verification in Intel $^{\scriptsize\circledR}$ CoreTM i7 Processor Execution Engine Validation, Proceedings of the 21st International Conference on Computer Aided Verification, CAV '09, pp.414-429, 2009.
DOI : 10.1109/FMCAD.2008.ECP.12

]. Keatley, A REVIEW OF THE FDA DRAFT GUIDANCE DOCUMENT FOR SOFTWARE VALIDATION: GUIDANCE FOR INDUSTRY, Quality Assurance, vol.7, issue.1, pp.49-55, 1999.
DOI : 10.1080/105294100277723

]. M. Khan, Rapid ECG Interpretation, pp.47-271, 2008.
DOI : 10.1007/978-1-59745-408-7

]. Kosara, S. Miksch, A. , A. Seyfang, and P. Votruba, Tools for Acquiring Clinical Guidelines in Asbru, 2002.

]. R. Kowalski, The Relation between Logic Programming and Logic Specification [and Discussion], Proc. of a discussion, pp.11-27, 1985.
DOI : 10.1098/rsta.1984.0064

. Kye-rok, Yeong Rak Seong Kye-Rok Jun and Tag Gon Kim. A Cellular Automata Model of Activation Process in Ventricular Muscle, pp.769-774, 1994.

]. L. Lamport, The temporal logic of actions, ACM Transactions on Programming Languages and Systems, vol.16, issue.3, pp.872-923, 1994.
DOI : 10.1145/177492.177726

]. L. Lamport, Specifying Systems: The TLA + + Language and Tools for Hardware and Software Engineers, 2002.

]. K. Lano, J. Bicarregui, and A. Sanchez, Invariant-based Synthesis and Composition of Control Algorithms using B. In FM'99 ? B Users Group Meeting ? Applying B in an industrial context: Tools, Lessons and Techniques, pp.69-86, 1999.

T. Gary, J. Leavens, D. Abrial, M. Batory, A. Butler et al., Roadmap for Enhanced Languages and Methods to Aid Verification, Fifth Intl. Conf. Generative Programming and Component Engineering, pp.221-235, 2006.

T. Thierry-lecomte, G. Servat, and . Pouzancre, Formal Methods in Safety-Critical Railway Systems. ClearSy, no. HCSS+, 2007.

G. Nancy, P. R. Leveson, and . Harvey, Software fault tree analysis, Journal of Systems and Software, vol.3, issue.2, pp.173-181, 1983.

N. G. Leveson, Software safety in embedded computer systems, Communications of the ACM, vol.34, issue.2, pp.34-46, 1991.
DOI : 10.1145/102792.102799

]. N. Leveson and C. S. Turner, An investigation of the Therac-25 accidents, Computer, vol.26, issue.7, pp.18-41, 1993.
DOI : 10.1109/MC.1993.274940

N. G. Leveson, M. Per, E. Heimdahl, S. Member, H. Hildreth et al., Requirements specification for process-control systems, IEEE Transactions on Software Engineering, vol.20, issue.9, pp.684-707, 1994.
DOI : 10.1109/32.317428

K. N. Lohr and M. J. Field, United States. and Institute of Medicine (U.S.) Clinical practice guidelines : directions for a new program / committee to advise the public health service on clinical practice guidelines, institute of medicine, 1990.

J. Charles and . Love, Cardiac pacemakers and defibrillators, pp.131-165, 2006.

H. Daniel-macedo, P. G. Larsen, and J. Fitzgerald, Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM, Proceedings of the 15th international symposium on Formal Methods (FM'08), Lecture Notes in Computer Science, pp.181-197, 2008.

H. Magee, Validation of medical modeling & simulation training devices and systems, Stud Health Technol Inform, vol.94, pp.196-204, 2003.

]. T. Maibaum and A. Wassyng, A Product-Focused Approach to Software Certification, Computer, vol.41, issue.2, pp.91-93, 2008.
DOI : 10.1109/MC.2008.37

H. William, M. O. Maisel, W. G. Sweeney, K. E. Stevenson, L. M. Ellison et al., Recalls and Safety Alerts Involving Pacemakers and Implantable Cardioverter-Defibrillator Generators, JAMA: The Journal of the American Medical Association, vol.286, issue.128, pp.793-799, 2001.

A. T. Valerio-panzica-la-manna, A. Bonanno, and . Motta, Poster on A simple pacemaker Implementation, 2009.

J. John and . Marciniak, Encyclopedia of software engineering, p.63, 2002.

G. Marcos, F. Berger, A. Van-harmelen, H. Ten-teije, S. Roomans et al., Using Critiquing for Improving Medical Protocols: Harder than It Seems, Proceedings of the 8th Conference on AI in Medicine in Europe: Artificial Intelligence Medicine, AIME '01, pp.431-441, 2001.
DOI : 10.1007/3-540-48229-6_59

A. Mashkoor, J. Jacquot, and J. Souquières, Transformation Heuristics for Formal Requirements Validation by Animation, 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems -SafeCert 2009, p.78, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00374082

. Matlab and . Matlab, SIMULINK -Simulation and Model Based Design, pp.225-239

R. Nancy, N. R. Mead, C. Mead, and . Scondras, International Liability Issues for Software Quality, pp.15-283, 2003.

D. Méry and N. , Pacemaker's Functional Behaviors in Event-B, MOSEL, pp.25-163, 0200.

D. Méry and N. Singh, EB2C : A Tool for Event-B to C Conversion Support, Poster and Tool Demo submission and published in a CNR Technical Report in SEFM, pp.284-286, 2010.

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

D. Méry and N. , Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. (http://hal.archivesouvertes .fr/inria-00465061, MOSEL, pp.163-172, 0200.

D. Méry and N. Singh, Trustable Formal Specification for Software Certification, Tiziana Margaria and Bernhard Steffen, pp.312-326, 2010.
DOI : 10.1002/9780470695982

D. Méry and N. Singh, A generic framework: from modeling to code, Innovations in Systems and Software Engineering, pp.1-9, 2011.
DOI : 10.1145/1125808.1125811

D. Méry and N. Singh, Automatic code generation from event-B models, Proceedings of the Second Symposium on Information and Communication Technology, SoICT '11, pp.283-284, 2011.
DOI : 10.1145/2069216.2069252

D. Méry and N. Singh, EB2J : Code Generation from Event-B to Java (Short Paper) in 14th Brazilian Symposium on Formal Methods (SBMF'11), pp.217-242, 2011.

D. Méry and N. Singh, Formal Development and Automatic Code Generation: Cardiac Pacemaker, International Conference on Computers and Advanced Technology in Education (ICCATE'11). Communications in Computer and Information Science (CCIS), pp.124-126, 2011.
DOI : 10.1115/1.859971.paper3

D. Méry and N. Singh, Formal Specification of Medical Systems by Proof-Based Refinement (in Press) ACM Transaction Embedded Computing Systems, 2011.

D. Méry and N. Singh, Formalisation of the Heart based on Conduction of Electrical Impulses and Cellular-Automata, International Symposium on Foundations of Health Information Engineering and Systems (FHIES'11). 2011. (Cited on pages 3, pp.130-132, 2011.

D. Méry and N. Singh, Functional Behavior of a Cardiac Pacing System, International Journal of Discrete Event Control Systems, vol.1, issue.2, pp.129-149, 0207.

D. Méry and N. Singh, Medical Protocol Diagnosis Using Formal Methods, International Symposium on Foundations of Health Information Engineering and Systems (FHIES'11). 2011. (Cited on pages 6, pp.274-275, 2011.
DOI : 10.1007/978-3-642-32355-3_1

D. Méry, N. Méry, /. Kumar-singh, and M. , Technical Report on Formalisation of the Heart using Analysis of Conduction Time and Velocity of the Electrocardiography and Cellular-Automata, pp.14-128, 2011.

D. Méry, N. Kumar-singh, /. , and M. , Technical Report on Interpretation of the Electrocardiogram (ECG) Signal using Formal Methods, pp.25-250, 2011.

M. Balser, Protocure: Supporting the Development of Medical Protocols through Formal Methods, Proceedings of the Symposium of Computerised Protocols and Guidelines, 2004.

]. Mili, J. Desharnais, and J. R. Gagné, Formal models of stepwise refinements of programs, ACM Computing Surveys, vol.18, issue.3, pp.231-276, 1986.
DOI : 10.1145/27632.28054

L. Perry and . Miller, A critiquing approach to expert computer advice: Attending, 1985.

]. S. Miller and M. Srivas, Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods, Proceedings of 1995 IEEE Workshop on Industrial-Strength Formal Specification Techniques, pp.2-16, 1995.
DOI : 10.1109/WIFT.1995.515475

P. Steven and . Miller, Specifying the mode logic of a flight guidance system in CoRE and SCR. In FMSP '98: Proceedings of the second workshop on Formal methods in software practice, pp.44-53, 1998.

D. W. Miller, S. J. Frawley, and P. L. Miller, Using semantic constraints to help verify the completeness of a computer-based clinical guideline for childhood immunization. Computer methods and programs in biomedicine, pp.267-280, 1999.

]. R. Milner, A calculus of communicating systems, 1982.
DOI : 10.1007/3-540-10235-3

]. L. Moreau and J. Duprat, A construction of distributed reference counting, Acta Informatica, vol.37, issue.8, pp.563-595, 2001.
DOI : 10.1007/PL00013315

]. C. Morgan, Programming from specifications. Prentice Hall International Series in Computer Science, 1990.

]. D. Parnas, On the criteria to be used in decomposing systems into modules, Communications of the ACM, vol.15, issue.12, pp.1053-1058, 1972.
DOI : 10.1145/361598.361623

]. M. Paulk, The capability maturity model: guidelines for improving the software process. The SEI series in software engineering, 1995.

P. David, J. Pearce, P. H. Kelly, and C. Hankin, Efficient field-sensitive pointer analysis of C, ACM Trans. Program. Lang. Syst, vol.30, issue.1, p.4, 2007.

M. Peleg, S. Tu, J. Bury, P. Ciccarese, J. Fox et al., Comparing Computer-interpretable Guideline Models: A Case-study Approach, Journal of the American Medical Informatics Association, vol.16, issue.2, 2003.
DOI : 10.1097/00002030-200201250-00010

B. Pérez and I. Porres, Authoring and verification of clinical guidelines: A model driven approach, Journal of Biomedical Informatics, vol.43, issue.4, pp.520-536, 2010.
DOI : 10.1016/j.jbi.2010.02.009

A. Platzer and J. Quesel, KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description), The International Joint Conference on Automated Reasoning (IJCAR), pp.171-178, 2008.
DOI : 10.1007/978-3-540-71070-7_15

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

]. C. Ponsard, P. Massonet, A. Rifaut, J. F. Molderez, A. Van-lamsweerde et al., Early Verification and Validation of Mission Critical Systems, Proceedings of the Ninth International Workshop on Formal Methods for Industrial Critical Systems, pp.237-254, 2004.
DOI : 10.1016/j.entcs.2004.08.067

]. D. Price, Pentium FDIV flaw-lessons learned, IEEE Micro, vol.15, issue.2, pp.86-88, 1995.
DOI : 10.1109/40.372360

. Prob and . Prob, The ProB Animator and Model Checker for the B Method. http://www.stups.uni-duesseldorf.de/ProB/overview, pp.162-238

R. Balasubramaniam and M. Jarke, Toward Reference Models for Requirements Traceability, IEEE Trans. Softw. Eng, vol.27, pp.58-93, 2001.

A. Crespo, Mode Change Protocols for Real-Time Systems: A Survey and a New Proposal, Real-Time Syst, vol.26, issue.2, pp.161-197, 2004.

R. Reinhardt and S. Dowd, Adobe Flash CS3 Professional Bible, page 1232, 2007.

]. Richter, CLR Via C#, Second Edition, 2006.

W. J. Horst, M. M. Rittel, and . Webber, Dilemmas in a general theory of planning, Policy Sciences, vol.4, issue.2, pp.155-169, 1973.

]. W. Royce, Managing the development of large software systems: concepts and techniques, Proceedings of the 9th international conference on Software Engineering, ICSE '87, pp.328-338, 1987.

]. Samson, M. A. Musen, S. W. Tu, K. Amar, Y. Das et al., EON: A Component-Based Approach to Automation of Protocol- Directed Therapy, 1996.

W. Scacchi, Managing Software Engineering Projects: A Social Analysis Software Engineering, IEEE Transactions on, issue.1, pp.49-59, 1984.

J. Ryser, S. Berner, M. Glinz, R. Reutemann, and E. Fahr, A Survey of Simulation Tools for Requirements Engineering, 2000.

]. Schmitt, A. Hoffmann, M. Balser, W. Reif, and M. Marcos, Interactive Verification of Medical Guidelines, Jayadev Misra, 2006.
DOI : 10.1007/11813040_3

]. J. Schumann, Automated theorem proving in software engineering, pp.35-65, 2001.
DOI : 10.1007/978-3-662-22646-9

W. Robert and . Sebesta, Concepts of programming languages, 2009.

]. E. Sekerinski and K. Sere, Program Development by Refinement -Cases Studies Using the B Method. FACIT, p.51, 1998.

A. Seyfang, S. M. Marcos, J. Wittenberg, C. Polo-conde, and K. Rosenbrand, Bridging the Gap between Informal and Formal Guideline Representations, Proceeding of the 2006 conference on ECAI 2006: 17th European Conference on Artificial Intelligence, pp.447-451, 2006.

S. Shahar, P. Miksch, and . Johnson, The Asgaard project: a task-specific framework for the application and critiquing of time-oriented clinical guidelines, Artificial Intelligence in Medicine, vol.14, issue.1-2, pp.29-51, 1998.
DOI : 10.1016/S0933-3657(98)00015-3

N. Richard, R. A. Shiffman, and . Greenes, Improving Clinical Guidelines with Logic and Decision-table Techniques: Application to Hepatitis Immunization Recommendations, Med Decis Making, vol.14, issue.3, pp.245-254, 1994.

N. Richard and . Shiffman, Representation of Clinical Practice Guidelines in Conventional and Augmented Decision Tables, Journal of the American Medical Informatics Association, vol.4, issue.5, pp.382-393, 1997.

I. Jawed, I. C. Siddiqi, C. R. Morrey, M. B. Roast, and . Ozcan, Towards quality requirements via animated formal specifications, Ann. Softw. Eng, vol.3, pp.131-155, 1997.

J. E. Smith, K. Mieczyslaw, K. Kokar, and . Baclawski, Formal Verification of UML Diagrams: A First Step Towards Code Generation, Practical UML-Based Rigorous Development Methods -Countering or Integrating the eXtremists, pp.224-240, 2001.

]. J. Spivey, Understanding Z: a specification language and its formal semantics, 1987.

]. R. Stärk, J. Schmid, and E. Börger, Java and the Java Virtual Machine, 1998.
DOI : 10.1007/978-3-642-59495-3

]. Stepney, D. Cooper, and J. Woodcock, An Electronic Purse: Specification, Refinement, and Proof, 2000.

M. Marcos, J. Balser, C. Van-croonenborg, F. Duelli, P. Van-harmelen et al., Improving medical protocols by formal methods, Artif. Intell. Med, vol.36, issue.3, pp.193-209, 2006.

J. Paul and . Trafford, The Use of Formal Methods for Safety-Critical System, pp.35-38, 1997.

K. Wijbrans and M. R. Chaudron, Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System Revisiting Seven Myths of Formal Methods, Formal Methods in System Design, vol.19, issue.2, pp.195-215, 2001.

A. Luu, M. C. Tuan, Q. Zheng, and . Tho, Modeling and Verification of Safety Critical Systems: A Case Study on Pacemaker. Secure System Integration and Reliability Improvement, pp.23-32, 2010.

]. D. Turner, Functional programs as executable specifications, Proc. of a discussion, pp.29-54, 1985.

H. T. Van, P. Van-lamsweerde, C. Massonet, and . Ponsard, Goal-Oriented Requirements Animation, Proceedings of the Requirements Engineering Conference, 12th IEEE International, pp.218-228, 2004.

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.

]. H. Walters, Hybrid implementations of algebraic specifications, Hélène Kirchner and Wolfgang Wechler Algebraic and Logic Programming, pp.40-54, 1990.
DOI : 10.1007/3-540-53162-9_29

M. Wang, S. W. Peleg, A. A. Tu, R. A. Boxwala, . Greenes et al., Representation primitives, process models and patient data in computer-interpretable clinical practice guidelines:, International Journal of Medical Informatics, vol.68, issue.1-3, pp.59-70, 2002.
DOI : 10.1016/S1386-5056(02)00065-5

]. J. Woodcock and R. Banach, The Verification Grand Challenge, Journal of Universal Computer Science, vol.13, issue.5 2, pp.661-668, 2007.

J. Woodcock, S. Stepney, D. Cooper, J. A. Clark, and J. Jacob, The certification of the Mondex electronic purse to ITSEC Level E6, Formal Aspects of Computing, vol.1, issue.4, pp.5-19, 2008.
DOI : 10.3233/JCS-1992-13-409

]. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald, Formal methods, ACM Computing Surveys, vol.41, issue.4, pp.1-19, 2009.
DOI : 10.1145/1592434.1592436

]. Wright, Automatic Generation of C from Event-B. In Workshop on Integration of Model-based Formal Methods and Tools IM_FMT'2009 -in IFM, 2009.

A. Hrs, Guidelines for Device-Based Therapy of Cardiac Rhythm Abnormalities: Executive Summary: A Report of the American College of CardiologyAmerican 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, Circulation, vol.117, issue.166, pp.2820-2840, 2008.

]. Xu and T. Maibaum, Generic Insulin Infusion Pump, International Symposium on Foundations of Health Information Engineering and Systems (FHIES'11). 2011, 2011.

]. Zhang, L. Paul, R. Jones, and . Jetley, A Hazard Analysis for a Generic Insulin Infusion Pump, Journal of Diabetes Science and Technology, vol.4, issue.2, pp.263-283, 2010.
DOI : 10.1177/193229681000400207