Biomedical Engineering Reference
In-Depth Information
error. For instance, overflow and underflow of bounded integer are run-time errors
that should be addressed in the proof process. For developing a critical system, an
automated technique based on formal methods have been matured to provide a high
degree of confidence. Introduction of a context file is a very important phase of the
code generation process, which provides one more level of refinement to make a
system specification deterministic. The deterministic model is known as concrete
well formed specification, which shows correct system behaviour before generating
the source code. New context file consists of all
primary data types
corresponding
to the programming languages (C, C++, Java and C#).
The papers [
15
,
16
,
35
] address a solution for the proof of clean termination
that provides the facts that a program is totally correct. Clean termination means
that a program terminates normally without any execution-time semantic errors like
integer overflow, use of undefined variables, subscript out of range, etc. [
16
,
35
].
We propose a pre-processing stage for obtaining a deterministic model using one
more level of refinement through introduction of a new context that is similar to
the clean termination approach [
15
,
35
]. This refinement phase provides the de-
terministic definitions of constants and variables. This new refinement generates a
lot of proof obligations. Types of generated proof obligations and proof details are
similar to the papers [
15
,
16
,
35
]. This level of refinement complies system speci-
fication abstractly. The generated proof obligations are discharged by automatic as
well as manual, and all proofs that are necessary to verify the specification in order
to guarantee the consistency and correctness of the system. Therefore, this phase
is very important to maintain all safety properties in the automatic code generation
process.
Selection of a Context File
This phase provides many context files, to add into a current project according to
a target programming language choice (C, C++, Java and C#). Table
7.1
shows
bounded integer data types for all target programming languages. In the Event-B
language, there are two kinds of constants and variables (
data
): abstract data and
concrete data. Abstract data consists in all the elements and sets that can be used
in set theory, as defined in Event-B (integers, enumerated sets, Cartesian products,
power sets, relations, and so on). They are mainly used at the higher levels of spec-
ification (machines and in top level refinements) [
2
].
Concrete data are those which may be used in the final translation process, each
time the data thus introduced will not be further refined in the development. It is
the case for constants and variables at the implementation level but also for param-
eters and results of operations, which cannot be refined in Event-B [
2
]. Concrete
data must match ordinary data types in a usual programming language because they
should be “implemented” directly in the target programming language. So, the cor-
respondence between concrete data and data types must be obvious. In standard
Event-B, they are the following ones:
Search WWH ::
Custom Search