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

• Possibility of annotating models for different purposes (e.g., directing synthesis

or hooking to verification tools).

• To discover the complex situation using refinement approach.

• Decomposition of the complex system into different independent subsystems.

• To reduce the gap between software engineers and stakeholders requirements us-

ing real-time animator and easy to explain model behaviour to domain experts as
well stakeholders.

• Ambiguous and incomplete requirements can be clarified and completed by

hands-on experience with the specifications using our approach.

Code generation is a process, which is used to transform a formal specifica-
tion into any programming language like C, C++, C#, Java, etc. Code generation
from the verified formal model is our main objective. For generating the source
code into different kinds of programming languages (C, C++, Java and C#), we
have used a tool EB2ALL [ 13 , 41 , 46 , 47 ]. We have developed a set of plug-ins
tools [ 13 , 41 , 46 , 47 ], which provides fully automatic code generation from Event-
B formal specification into programming languages. The adaptations of the transla-
tion rules are required more complete experiments, especially with the large formal
models for checking the impact on the execution time for some specific platforms.
Finally, we have shown a satisfactory result and demonstrate the ability to generate
automatically source code from E VENT B specification of the cardiac pacemaker in
C, C++, Java and C# languages, which are comparable to a code written by hand
with ordinary programming languages. The gains rely then on the guarantees pro-
vided using formal methods 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/space efficient as handwritten code.
This chapter also presents an approach for modelling the closed-loop system of
the cardiac pacemaker. The prime objective of this approach is to provide a new
modelling technique, which helps to combine the formal models of a critical sys-
tem and related environment. For example, the cardiac pacemaker operates in the
biological heart system. The closed-loop modelling is an effective approach, which
guarantees the correctness of the operating behaviour of the critical system. More-
over, this approach can be viable to obtain the certification standards for the de-
veloping system. To build a closed-loop model using both environment and device
modelling is considered as a standard approach for validation, given that designing
an environment model is a challenging problem in the real world. Industry has long
sought such an approach to validating system models in a biological environment.
Proposed development methodology and associated techniques and tools enable
us to design a new environment for medical device modelling and simulating and
offers to obtain that challenge of complying with FDA's QSR and ISO's 13485
quality system directives [ 23 , 32 ].
In order to assess the overall utility of our approach, a selection of the results of
the formalisation and verification steps have been presented to a group of pacemaker
developers (French-Italian based pacemaker company). The developers are satisfied
by the results of pacemaker development using all proposed approaches in sense of