Introduction - Using Event-B for Critical Device Software Systems - page 4

code from the verified system specifications and final phase is used for acceptance
testing of the developed system. This approach is useful to verify complex proper-
ties of a system and to discover the potential problems like deadlock and liveness at
an early stage of the system development.
According to the development life cycle of a critical system, we emphasise the
requirements traceability using a real-time animator [ 19 ]. Formal modelling of re-
quirements is a challenging task, which is used to reasoning in earlier phases of the
system development to make sure completeness, consistency, and automated veri-
fication of the requirements. The real-time animation of a formal model has been
recognised to be a promising approach to support the process of validation of re-
quirement's specification. The principle is to simulate the desired behaviours of a
given system using formal models in the real-time environment and to visualise
the simulation in some form which appeals to stakeholders. The real-time environ-
ment assists in the construction, clarification, validation and visualisation of a formal
specification. Such an approach is also useful for evidence-based certification.
Refinement techniques [ 1 , 2 , 4 ] serve a key role for modelling a complex system
in an incremental way. A refinement chart is a graphical representation of a complex
system using a layering approach, where functional blocks are divided into multiple
simpler blocks in a new refinement level, without changing the original behaviour
of the system. The final goal of using this refinement chart is to obtain a specifi-
cation that is detailed enough to be effectively implemented, but also to correctly
describe the system behaviours. The purpose of the refinement chart is to provide
an easily manageable representation for different refinements of the systems. The
refinement chart offers a clear view of assistance in “system” integration. This ap-
proach also gives a clear view about the system assembly based on operating modes
and different kinds of features. This is an important issue not only for being able to
derive system-level performance and correctness guarantees, but also for being able
to assemble components in a cost-effective manner.
Another important step in the software-development life cycle is the code im-
plementation. In this context, we have developed an automatic code generation
tool [ 7 , 18 , 22 , 23 ] for generating an efficient target programming language code
(C, C++, Java and C#) from Event-B formal specifications related to the analysis of
complex problems. This tool is a collection of plug-ins, which are used for translat-
ing Event-B formal specifications into different kinds of programming languages.
The translation tool is rigorously developed with safety properties preservation. We
present an architecture of the translation process, to generate a target language code
from Event-B models using Event-B grammar through syntax-directed translation,
code scheduling architecture, and verification of an automatic generated code.
A closed-loop model of a system is considered as a de facto standard for crit-
ical systems in the medical, avionic, and automotive domains for validating the
system model at the early stages of system development, which is an open prob-
lem in the area of modelling. The cardiac pacemaker and implantable cardioverter-
defibrillators (ICDs) are key critical medical devices, which require closed-loop
modelling (integration of system and environment modelling) for verification pur-
pose to obtain a certificate from the certification bodies. In this context, we propose