Introduction - Using Event-B for Critical Device Software Systems - page 6

tool; EB2ALL [ 7 , 18 , 22 , 23 , 28 ]. In Chap. 8 , we present a methodology to model
a biological system, like the heart. The heart model is mainly based on electrocar-
diography analysis, which models the heart system at the cellular level. The main
objective of this methodology is to model the heart system and integrate it with the
medical device model like the cardiac pacemaker to specify a closed-loop system.
Chapter 9 presents a complete formal development of a cardiac pacemaker using
proposed techniques and tools from requirements analysis to automatic code gen-
eration. In Chap. 10 , we present a new application of formal methods to evaluate
real-life medical protocols for quality improvement. An assessment of the proposed
approach is given through a case study, relative to a real-life reference protocol
(ECG Interpretation) which covers a wide variety of protocol characteristics related
to several heart diseases. We formalise the given reference protocol, verify a set of
interesting properties of the protocol and finally determine anomalies. Chapter 11
summarises this topic.
References
1. Abrial, J.-R. (1996). The B-book: Assigning programs to meanings . New York: Cambridge
University Press.
2. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
3. Acuña, S. T., & Juristo, N. (2005). International series in software engineering. Software
process modeling . New York: Springer.
4. Back, R. J. R. (1981). On correct refinement of programs. Journal of Computer and System
Sciences , 23 (1), 49-68.
5. Bell, R., & Reinert, D. (1993). Risk and system integrity concepts for safety-related control
systems. Microprocessors and Microsystems , 17 , 3-15.
6. CC. Common criteria. http://www.commoncriteriaportal.org/ .
7. EB2ALL (2011). Automatic code generation from Event-B to many programming languages.
http://eb2all.loria.fr/ .
8. FDA. Food and Drug Administration. http://www.fda.gov/ .
9. Gaudel, M.-C., & Woodcock, J. (Eds.) (1996). Lecture notes in computer science: Vol. 1051 .
Proceedings, FME'96: Industrial benefit and advances in formal methods . Third international
symposium of formal methods Europe, co-sponsored by IFIP WG 14.3, Oxford, March 18-22,
1996. Berlin: Springer.
10. Gibbs, W. W. (1994). Software's chronic crisis. Scientific American , September.
11. 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 .
12. IEEE-SA. IEEE Standards Association. http://standards.ieee.org/ .
13. ISO. International Organization for Standardization. http://www.iso.org/ .
14. Jetley, R., Purushothaman Iyer, S., & Jones, P. (2006). A formal methods approach to medical
device review. Computer , 39 (4), 61-67.
15. Leveson, N. G. (1991). Software safety in embedded computer systems. Communications of
the ACM , 34 , 34-46.
16. Leveson, N. G., & Turner, C. S. (1993). An investigation of the Therac-25 accidents. Com-
puter , 26 , 18-41.
17. Méry, D., & Singh, N. K. (2009). Pacemaker's functional behaviors in Event-B
(Research report). MOSEL-LORIA-INRIA-CNRS: UMR7503-Université Henri Poincaré-