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

incremental development, real-time animation of formal model, integration of hard-
ware and software and automatically code generation approach from verified formal
specifications. They are really agreed on the refinement charts for showing operat-
ing mode relation and their mode transitions. Based on the experiment described
above and our conclusions we are convinced of the usefulness on certain areas, and
therefore, we are considering to use all these tools and methodology, which are very
helpful to design not even in a medical domain but also for other industrial domains,
such as avionic and automotive domains.
References
1. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
2. Artigou, J. Y., & Monsuez, J. J. (2007). Cardiologie et maladies vasculaires . Paris: Elsevier
Masson.
3. Baier, C., & Katoen, J.-P. (2008). Principles of model checking (representation and mind
series) . Cambridge: MIT Press.
4. Barold, S. S., Stroobandt, R. X., & Sinnaeve, A. F. (2004). Cardiac pacemakers step by step .
London: Futura. ISBN 1-4051-1647-1.
5. Bayes, B. V. N., de Luna, A., & Malik, M. (2006). The morphology of the electrocardiogram.
In The ESC textbook of cardiovascular medicine (pp. 1-36). Oxford: Blackwell.
6. Bjørner, D., & Jones, C. B. (Eds.) (1978). The Vienna development method: The meta-
language . London: Springer.
7. Boston Scientific (2007). Pacemaker system specification (Technical report). http://www.cas.
mcmaster.ca/sqrl/~SQRLDocuments/PACEMAKER.pdf .
8. Cansell, D., & Méry, D. (2008). The Event-B modelling method: Concepts and case studies.
In D. Bjørner & M. C. Henson (Eds.), Monographs in theoretical computer science . Logics of
specification languages (pp. 47-152). Berlin: Springer.
9. Cansell, D., Méry, D., & Rehm, J. (2006). Time constraint patterns for Event B develop-
ment. In J. Julliand & O. Kouchnarenko (Eds.), Lecture notes in computer science: Vol. 4355 .
B 2007: Formal specification and development in B (pp. 140-154). Berlin: Springer.
10. Clarke, E. M., Grumberg, O., & Peled, D. (2001). Model checking . Cambridge: MIT Press.
11. CC. Common criteria. http://www.commoncriteriaportal.org/ .
12. Crocker, D. (2003). Perfect developer: A tool for object-oriented formal specification and
refinement. Tools exhibition notes at formal methods Europe. In Tools exhibition notes at
formal methods Europe (p. 2003).
13. EB2ALL (2011). Automatic code generation from Event-B to many programming languages.
http://eb2all.loria.fr/ .
14. Ellenbogen, K. A., & Wood, M. A. (2005). Cardiac pacing and ICDs (4th ed.). Oxford: Black-
well. ISBN 1-4051-0447-3.
15. Epstein, A. E., DiMarco, J. P., Ellenbogen, K. A., Estes, N. A. M., III, Freedman, R. A.,
Gettes, L. S., et al. (2008). ACC/AHA/HRS 2008 guidelines for device-based therapy of car-
diac rhythm abnormalities: 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 de-
vices) developed in collaboration with the American Association for Thoracic Surgery and
Society of Thoracic Surgeons. Journal of the American College of Cardiology , 51 (21), e1-
e62.
16. FDA. Food and Drug Administration. http://www.fda.gov/ .