Conclusion - Using Event-B for Critical Device Software Systems - page 300

the target programming languages. The benefits of developing and enhancing the
translation tool [ 3 , 14 , 16 , 17 ] presented stem primarily from their increased sup-
port for automated translation between the two components of a formal model and
target programming language. The adaptations of the translation rules require more
complete experiments, especially with large formal models for checking the impact
on the execution time for some specific platforms. The gains rely then on the guar-
antees provided using a formal method and on the certification level which can be
obtained by this way. As far as we know, only few formal methods support code
generation, which is as time and space efficient as handwritten code.
Development of an environment for closed-loop modelling using formal tech-
niques [ 21 ] is our another remarkable contribution of this topic. We have pre-
sented a methodology for modelling a mathematical heart model based on logico-
mathematical theory. The most important goal is that this formal model helps to ob-
tain a certification for the medical devices related to the heart system such as cardiac
pacemaker and ICDs. It can be also used as a diagnostic tool to identify a critical
state of the patient using a patient environment model. The heart model is based
on electrocardiography analysis, which models the heart circulatory system at the
cellular level. This has been one of the most challenging problems to validate and
verify the correct behaviour of the developed system model (a cardiac pacemaker
or ICDs) under biological environment (i.e. heart). This approach for formalising
and reasoning about impulse propagation into the heart system through the conduc-
tion network. The heart model suggests that such an approach can yield a viable
model that can be subjected to useful validation against medical device software at
an early stage in the development process (i.e. cardiac pacemaker). The heart model
is verified with the help of physiologist and cardiologist experts.
11.4 Applications
Assessment of proposed development life-cycle methodology and a set of associ-
ated techniques and tools are made through the development of the industrial-scale
case study, which cover medical domains. The well-known case study is the cardiac
pacemaker [ 13 , 15 , 18 ]. We have applied development methodology and associ-
ated techniques and tools for system implementation. The combined approaches
of the formal verification, and validation, refinement chart, real-time animator, and
automatic code generation, cover enumerated claims like certifiable assurance and
safety, error-free system development and system integration. Refinement chart spe-
cially covers component-based design frameworks and decomposition, integration
of critical infrastructure and device integration. Our case study on cardiac pace-
maker illustrates the potential value of a formal specification, and its subsequent
animation can bring to the comprehension and clarification of the informal require-
ments. The case study has shown that requirement specifications could be used di-
rectly in real-time environment without modifications for automatic test result eval-
uation using our approach. We can see from our pacemaker case study that all these