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

a methodology to model a biological system related to the heart system, which pro-
vides a biological environment for building the close loop system for the cardiac
pacemaker [ 27 ]. The heart model is mainly based on electrocardiography analy-
sis, which models the heart system at the cellular level. The main objective of this
methodology is to model the heart system and integrate with a medical device model
like the cardiac pacemaker to specify a closed-loop model. Industries have been
striving for such a kind of approach for a long time in order to validate a system
model under the virtual biological environment [ 27 ].
Assessment of the proposed framework, and techniques and tools are scrutinised
through the development of a cardiac pacemaker. The cardiac pacemaker is a pilot
project of the international “Grand Challenge”. This topic covers a complete devel-
opment process of a cardiac pacemaker using the proposed life-cycle framework and
developed tools [ 17 , 20 , 24 ] from requirements analysis to code implementation.
Formal techniques are useful not only for critical-systems, but it can be used
to verify required safety properties in other domains, for example, in the clinical
domain to verify the correctness of protocols and guidelines [ 26 , 27 , 30 ]. Clinical
guidelines systematically assist practitioners with providing appropriate health care
for specific clinical circumstances. Today, a significant number of guidelines and
protocols are lacking in quality. Indeed, ambiguity, and incompleteness are com-
mon anomalies in the medical practices. Our main objective is to find anomalies
and to improve the quality of medical protocols using well-known mathematical
formal techniques, such as Event-B. In this study, we use the Event-B modelling
language to capture guidelines for their validation for improving the protocols. An
appropriateness of the formalism is given through a case study, relative to a real-
life reference protocol (ECG Interpretation) that covers a wide variety of protocol
characteristics related to several heart diseases.
1.2.1 Outline
The topic is structured in 11 chapters. Chapter 2 presents a basic background and de-
velopment life-cycle related to the safety critical systems. Chapter 3 describes mod-
elling techniques using the Event-B modelling language. In Chap. 4 , we propose
a development life-cycle methodology for developing the highly critical software
systems using formal methods from requirements analysis to code implementation
using rigorous safety assessments. In Chap. 5 , we propose a novel architecture to
validate the formal model with real-time data set in the early stage of develop-
ment without generating the source code [ 19 ]. This architecture can be used for
requirement traceability. In Chap. 6 , the refinement chart is proposed to handle the
complexity and for designing the critical systems. In Chap. 7 , we present a tool
that automatically generates efficient target programming language code (C, C++,
Java and C#) from Event-B formal specification related to the analysis of complex
problems. In this chapter, the basic functionality as well as the design-flow is de-
scribed, stressing the advantages when designing this automatic code generation