Conclusion - Using Event-B for Critical Device Software Systems - page 298

based on formal methods support refinement based formal development, essential
verification, and validation steps and automatic code generation in the process of
critical system development. The proposed techniques and tools are the develop-
ment methodology, framework for real-time animator [ 15 ], refinement chart [ 24 ],
automatic code generation tools [ 3 , 14 , 16 , 17 ], and formal logic based heart model
for closed-loop modelling [ 19 , 21 , 22 ].
In Chap. 1 , we have given a list of objectives, which all are covered in this topic
through giving a new development life-cycle methodology and a set of associated
techniques and tools for developing the critical systems. Assessment of the develop-
ment methodology and a set of techniques and tools are given through well known
case study related to the medical domain. This work has established a unified the-
ory for the critical system development, and proposed techniques and tools fulfil
the other objectives. We have given a rigorous approach for the system develop-
ment rather than the traditional development of critical systems. In traditional de-
velopment, formal methods are used to provide safety assurances and to meet the
requirements of the standard of the certification bodies. Our new approach based
completely on formal techniques, develops the whole system rigorously from re-
quirement analysis to code implementation, satisfying all requirements of the stan-
dard certification bodies. In addition, the methodology provides a safety assessment
approach to analyse the whole development life cycle of the critical system, which
meets requirements of the certification standard bodies.
Complexity of the critical system makes, it is hard to understand and to verify.
Several approaches exist for the verification of critical systems, including model
checking, theorem proving, or simulation based validation. There exists a vast vari-
ety of problems related to the critical systems and several solutions for each prob-
lem. Rigorous reasoning about the system behaviour is required to ensure that a
desired behaviour is achieved. Event-B is a modelling language, which describes
a system abstractly, and introduces system details through refinement steps to ob-
tain the final concrete system. The Rodin [ 1 , 25 ] tools provide significant automated
proof support for generating the proof obligations and discharging them. Generated
proof obligations help to understand the complexity of the problem and to ensure the
correctness of the system. In the following sections, we have made several contribu-
tions towards an integration of refinement based development using Event-B with
formal specification, verification and code implementation for the critical systems.
11.2 Life-Cycle Methodology
A major step forward is the new life-cycle methodology, exploits the mathematical
base to carry out a complete rigorous proof based system development using formal
techniques in every step from requirement analysis to automatic code generation.
This life-cycle methodology is used for developing the critical systems for obtaining
the certificate standards, such as IEC-62304 [ 7 ] and the Common Criteria [ 2 , 4 , 12 ].
This development methodology combines the refinement approach with verification