The Cardiac Pacemaker - Using Event-B for Critical Device Software Systems - page 236

17. Gamma, E., Helm, R., Johnson, R., Vlissides, R., & Gamma, P. (1994). Design patterns: El-
ements of reusable object-oriented software design patterns . Reading: Addison-Wesley Pro-
fessional.
18. Goldman, B. S., Noble, E. J., Heller, J. G., & Covvey, D. (1974). The pacemaker challenge.
CMAJ. Canadian Medical Association Journal , 110 (1), 28-31.
19. Gomes, A., & Oliveira, M. (2009). Formal specification of a cardiac pacing system. In A. Cav-
alcanti & D. Dams (Eds.), Lecture notes in computer science: Vol. 5850 . FM 2009: Formal
methods (pp. 692-707). Berlin: Springer.
20. Gomes, A. O., & Oliveira, M. V. M. (2010). Formal development of a cardiac pacemaker:
From specification to code. In Lecture notes in computer science . SBFM 2010 (pp. 213-228).
21. Harrild, D. M., & Henriquez, C. S. (2000). A computer model of normal conduction in the
human atria. Circulation Research , 87 , 25-36.
22. Hesselson, A. (2003). Simplified interpretations of pacemaker ECGs . Oxford: Blackwell.
ISBN 978-1-4051-0372-5.
23. 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 .
24. Hoare, C. A. R. (2003). The verifying compiler: A grand challenge for computing research.
In H. Kosch, L. Böszörményi, & H. Hellwagner (Eds.), Lecture notes in computer science:
Vol. 2790 . Euro-Par 2003 parallel processing (p. 1). Berlin: Springer.
25. Hoare, C. A. R., Misra, J., Leavens, G. T., & Shankar, N. (2009). The verified software initia-
tive: A manifesto. ACM Computing Surveys , 41 (4), 22:1-22:8.
26. IEEE-SA. IEEE Standards Association. http://standards.ieee.org/ .
27. ISO. International Organization for Standardization. http://www.iso.org/ .
28. Jackson, D. (2002). Alloy: A lightweight object modelling notation. ACM Transactions on
Software Engineering and Methodology , 11 (2), 256-290.
29. Jiang, Z., Pajic, M., & Mangharam, R. (2011). Model-based closed-loop testing of implantable
pacemakers. In 2011 IEEE/ACM international conference on cyber-physical systems , ICCPS
(pp. 131-140).
30. Jiang, Z., Pajic, M., Moarref, S., Alur, R., & Mangharam, R. (2012). Modeling and verification
of a dual chamber implantable pacemaker. In C. Flanagan & B. König (Eds.), Lecture notes
in computer science: Vol. 7214 . Tools and algorithms for the construction and analysis of
systems (pp. 188-203). Berlin: Springer.
31. Kantharia, B. K., & Kutalek, S. P. (1999). Optimal programming of rate modulation functions.
Cardiac Electrophysiology Review , 3 , 53-55. doi: 10.1023/A:1009935600754 .
32. Keatley, K. L. (1999). A review of the FDA draft guidance document for software validation:
Guidance for industry. Quality Assurance , 7 (1), 49-55.
33. Khan, M. G. (2008). Rapid ECG interpretation . Clifton: Humana Press.
34. La Manna, V. P., Bonanno, A. T., & Motta, A. (2009). Poster on a simple pacemaker imple-
mentation. New York: ACM.
35. Lee, I., Pappas, G. J., Cleaveland, R., Hatcliff, J., Krogh, B. H., Lee, P., et al. (2006). High-
confidence medical device software and systems. Computer , 39 (4), 33-38.
36. Leuschel, M., & Butler, M. (2003). Lecture notes in computer science . ProB: A model checker
for B (pp. 855-874). Berlin: Springer.
37. Love, C. J. (2006). Cardiac pacemakers and defibrillators . Georgetown: Landes Bioscience.
ISBN 1-57059-691-3.
38. Macedo, H. D., Larsen, P. G., & Fitzgerald, J. (2008). Incremental development of a distributed
real-time model of a cardiac pacing system using VDM. In Lecture notes in computer science .
Proceedings of the 15th international symposium on formal methods , FM'08 (pp. 181-197).
Berlin: Springer.
39. Malmivuo, J. (1995). Bioelectromagnetism . Oxford: Oxford University Press. ISBN 0-19-
505823-2.
40. Méry, D., & Singh, N. K. (2009). Pacemaker's functional behaviors in Event-B
(Research report). MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-