Real-Time Animator and Requirements Traceability - Using Event-B for Critical Device Software Systems - page 91

• ability to monitor a real-time environment using animator at animation time and

analyse the requirements, violations of goals, expectations on the environments,
and domain properties.

This work has been influenced by guiding principles and technical benefits of
the formal system engineering, which offers participation of both software engi-
neers and user stakeholders that helps to move closer towards a quality requirements
specification and to develop an error-free system.

References

1. Abrial, J.-R. (2010). Modeling in Event-B: System and software engineering (1st ed.). New
York: Cambridge University Press.
2. Aizenbud-Reshef, N., Nolan, B. T., Rubin, J., & Shaham-Gafni, Y. (2006). Model traceability.
IBM Systems Journal , 45 (3), 515-526.
3. Balzer, R. M., Goldman, N. M., & Wile, D. S. (1982). Operational specification as the basis
for rapid prototyping. Software Engineering Notes , 7 , 3-16.
4. Berzins, V., Luqi, & Yehudai, A. (1993). Using transformations in specification-based proto-
typing. IEEE Transactions on Software Engineering , 19 (5), 436-452.
5. Bjørner, D., & Jones, C. B. (Eds.) (1978). The Vienna development method: The meta-
language . London: Springer.
6. Blaauboer, F., Sikkel, K., & Aydin, M. N. (2007). Deciding to adopt requirements traceabil-
ity in practice. In Proceedings of the 19th international conference on advanced information
systems engineering , CAiSE'07 (pp. 294-308). Berlin: Springer.
7. Bloomfield, R. E., & Froo, P. K. D. (1986). The application of formal methods to the assess-
ment of high integrity software. IEEE Transactions on Software Engineering , 12 , 988-993.
8. Boehm, B. W. (1981). Software engineering economics (1st ed.). Upper Saddle River: Prentice
Hall.
9. Bubenko, J. A., Jr. (1995). Challenges in requirements engineering. In Proceedings of the
second IEEE international symposium on requirements engineering (pp. 160-162).
10. 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.
11. CC. Common criteria. http://www.commoncriteriaportal.org/ .
12. CDRH (2006). Safety of marketed medical devices. Center for Devices and Radiological
Health, US FDA.
13. Clocksin, W. F., & Mellish, C. S. (1987). Programming in Prolog . New York: Springer.
14. Davis, A. M. (1992). Operational prototyping: A new development approach. IEEE Software ,
9 , 70-78.
15. Dorticós, F., Quiones, M. A., Tornes, F., Fayad, Y., Zayas, R., Castro, J., et al. (2006). Rate-
responsive pacing controlled by the TVI sensor in the treatment of sick sinus syndrome. In
A. Raviele (Ed.), Cardiac arrhythmias 2005 (pp. 581-590). Milan: Springer.
16. FDA. Food and Drug Administration. http://www.fda.gov/ .
17. Feather, M. S., Fickas, S., Van Lamsweerde, A., & Ponsard, C. (1998). Reconciling system
requirements and runtime behavior. In Proceedings of the 9th international workshop on soft-
ware specification and design , IWSSD'98 (p. 50). Washington: IEEE Comput. Soc.
18. Fickas, S., & Feather, M. S. (1995). Requirements monitoring in dynamic environments. In
Proceedings of the second IEEE international symposium on requirements engineering ,RE'95
(p. 140). Washington: IEEE Comput. Soc.