EB2ALL: An Automatic Code Generation Tool - Using Event-B for Critical Device Software Systems - page 110

7.3.3 Generated Proof Obligations
Introduction of a new context file is used as a data refinement of the system through
removing all the abstract data types into a selected target programming language us-
ing concrete data types. The refinement is supported by the Rodin [ 4 , 32 ] platform
guarantees the preservation of safety properties. Thus, the behaviour of the final
system is preserved by an abstract model as well as in the correctly refined models.
A lot of proof obligations are generated, which can prove automatically as well as
through manual intervention using interactive proof procedures [ 2 , 4 ]. A model de-
veloper can discharge all the generated proof obligations with the help of the Rodin
proof tool [ 32 ]. For example, when a set of constants and variables based on ab-
stract data types changes into the concrete data types in a new refinement level, then
some proof obligations are generated due to restrictive set of data ranges according
to the predefined system behaviours. All these new generated proof obligations are
required to discharge before continue the process. There is no guarantee to preserve
all the safety properties (related to overflow or underflow) of the proved system
unless all proof obligations are discharged.
Refinement using a context file provides proof of absence of run time errors into
the generated code. Such kind of approach is also known as formal code verifica-
tion [ 14 ]. Formal code verification techniques are used to demonstrate that at every
point in the code where a run time error may occur like numeric overflow or under-
flow. A set of required conditions as in the form of predicates guarantees that the
run time error will not occur. One more level of refinement approach is a very valu-
able step in the translation process to save from run time error, which demonstrates
that especially in systems where the occurrence of an undesired run time error is
unrecoverable.
7.3.4 Filter Context and Concrete Machine Modules
Refinement is a key feature of a formal development that supports incremental de-
velopment for specifying a complex system. Event-B modelling language supports
refinement based incremental development of a system, where a formal model is a
series of development starting with a very abstract model of the system under de-
velopment. Details are gradually added to this first model by building a sequence
of more concrete events and ending with the implementation of machine as a final
concrete system. The relationship between two successive models in this sequence
is refinement [ 2 , 4 ]. Relations between modules are only relations sees and refines .
This stage of the automatic translation process is used to filter all context and
concrete machine files from the selected project. The context files consist of static
properties as sets , constants , functions and enumerated sets of a system, while the
machine files contain dynamic properties as variables , functions and events of a sys-
tem. A set of filtered context and concrete files contains concrete sets , concrete con-
stants , concrete variables , concrete functions and concrete events , which are used