Conclusion - Using Event-B for Critical Device Software Systems - page 302

but it may be applicable to covering a large group of other categories (i.e. treatment,
management, prevention, counselling, evaluation, etc.) 1 related to the medical pro-

tocols.

References

1. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
2. CC. Common criteria. http://www.commoncriteriaportal.org/ .
3. EB2ALL (2011). Automatic code generation from Event-B to many programming languages.
http://eb2all.loria.fr/ .
4. Farn, K.-J., Lin, S.-K., & Fung, A. R.-W. (2004). A study on information security management
system evaluation—assets, threat and vulnerability. Computer Standards & Interfaces , 26 (6),
501-513.
5. FDA. Food and Drug Administration. http://www.fda.gov/ .
6. High Confidence Software and Systems Coordinating Group (2009). High-confidence medi-
cal devices: Cyber-physical systems for 21st century health care (Technical report). NITRD.
http://www.nitrd.gov/About/MedDevice-FINAL1-web.pdf .
7. IEC62304 (2006). International Electrotechnical Commission: Medical device software—
software life-cycle processes. http://www.iec.ch/ .
8. IEEE-SA. IEEE Standards Association. http://standards.ieee.org/ .
9. ISO. International Organization for Standardization. http://www.iso.org/ .
10. Keatley, K. L. (1999). A review of the FDA draft guidance document for software validation:
Guidance for industry. Quality Assurance , 7 (1), 49-55.
11. Leveson, N. G. (1991). Software safety in embedded computer systems. Communications of
the ACM , 34 , 34-46.
12. Mead, N. R., Mead, N. R., & Scondras, C. (2003). International liability issues for software
quality .
13. Méry, D., & Singh, N. K. (2009). Pacemaker's functional behaviors in Event-B
(Research report). MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-
Nancy I-Université Nancy II-Institut National Polytechnique de Lorraine. http://hal.inria.fr/
inria-00419973/en/ .
14. Méry, D., & Singh, N. K. (2010). EB2C: A tool for Event-B to C conversion support .Poster
and tool demo submission, published in a CNR technical report in SEFM.
15. Méry, D., & Singh, N. K. (2010). Real-time animation for formal specification. In M. Aiguier,
F. Bretaudeau, & D. Krob (Eds.), Complex systems design & management (pp. 49-60). Berlin:
Springer.
16. Méry, D., & Singh, N. K. (2011). Automatic code generation from Event-B models. In Pro-
ceedings of the second symposium on information and communication technology ,SoICT'11
(pp. 179-188). New York: ACM.
17. Méry, D., & Singh, N. K. (2011). EB2J: Code generation from Event-B to Java . Short paper
presented at the 14th Brazilian symposium on formal methods, SBMF'11.
18. Méry, D., & Singh, N. K. (2011). Functional behavior of a cardiac pacing system. Interna-
tional Journal of Discrete Event Control Systems , 1 (2), 129-149.
19. Méry, D., & Singh, N. K. (2011). Technical report on formalisation of the heart using analysis
of conduction time and velocity of the electrocardiography and cellular-automata. MOSEL-
LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-Nancy I-Université Nancy II-
Institut National Polytechnique de Lorraine. http://hal.inria.fr/inria-00600339/en/ .

1 http://www.guideline.gov/ .