Biomedical Engineering Reference
In-Depth Information
One- and two-electrode Pacemaker's pacing and sensing behaviours are validated
through cardiologist experts using real-time data; ECG signal. We have found some
unexpected behaviours of the formal model according to the cardiologist experts in
visualisation. We have modified the pacemaker formal model according to cardiol-
ogist experts and verify through the real-time animation tool. So, we consider that
the real-time animation tool has a very important role in the area of development of
the formal methods, and it can help to obtain a trust-able formal model, which can
be helpful to obtain the certification assurances [
11
,
16
,
23
,
26
,
27
,
44
].
9.13 Code Generation Using EB2ALL Tool
We have presented a proof-based an incremental formal development of a cardiac
pacemaker in [
40
,
43
,
48
,
53
] using our proposed tool and techniques. This section
presents an automatic code generation from developed and proved formal specifi-
cation of a cardiac pacemaker. We now illustrate the use of EB2C, EB2C++, EB2J
and EB2C# tools [
13
,
41
,
46
,
47
] by means of the automatic generation of C, C++,
Java and C# codes for the cardiac pacemaker system described with E
VENT
B
in [
45
,
51
]. This tool has a technique of automatic support of safety assurance of
a generated code. To achieve a verified source code of the cardiac pacemaker, we
have done further refinement of the concrete models of the cardiac pacemaker us-
ing a new context, which has some data ranges (see Table
7.1
) corresponding to the
programming languages. The context file provides deterministic ranges for all kinds
of data types. This refinement makes the model deterministic and generates some
proof obligations due to defining the fixed data ranges of all constants and variables
of the cardiac pacemaker model. The generated proof obligations are discharged by
automatic as well as manual, and all these proofs are necessary to verify the specifi-
cation in order to guarantee the consistency and correctness of the system. We have
discharged all the generated proof obligations before generating the source code.
This level of refinement complies system specification abstractly. Now, we move
to the next level of code translation methodology as to pass the concrete model for
continuing translation process.
The code translation from Event-B formal specification into any programming
language using EB2ALL is straightforward using a set of plug-ins (EB2C, EB2C++,
EB2J and EB2C#) [
13
,
41
,
46
,
47
]. The main idea is to translate an Event-B model
into any programming language code using the last concrete model. The EB2ALL
tool generates programming language files corresponding to the concrete models.
A generated source file using EB2ALL tool has a basic structure: a set of con-
stants, variables and functions. A set of constants and variables are extracted from
the context and machines sections of the Event-B model of the cardiac pacemaker,
respectively. Data type of constant is defined as an axiom in Event-B model. Simi-
larly, data type of variable is extracted from the invariant section of the model. Initial
value of the constants and variables are initialised, if their initial values are declared.
A set of constants and variables are given as follows, which are excerpted from the
translated 'C' codes of the cardiac pacemaker model.
Search WWH ::
Custom Search