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

and security is required to make amenable to the critical systems. A system is con-
sidered to accomplish the current task safely in case of a system failure. A formal
rigorous reasoning about algorithms and mechanisms beneath such a system is re-
quired to precisely understand the behaviour of systems at the design level. How-
ever, to develop a reliable system is a significantly complicated task, which affects
the reliability of a system.
Formal methods-based development [ 9 , 14 , 37 ] is a standard and popular ap-
proach to deal with the increasing complexity of a system with assurance of cor-
rectness in the modern software engineering practices. Formal methods-based tech-
niques increasingly control safety-critical functionality in the development of the
highly critical systems. These techniques are also considered as a way to meet the
requirements of the standard certificates [ 6 , 8 , 12 , 13 ] to evaluate a critical system
before use in practice. Furthermore, critical systems can be effectively analysed at
early stages of the development, which allows to explore conceptual errors, ambigu-
ities, requirements correctness, and design flaws before implementation of an actual
system. This approach helps to correct errors more easily and with less cost. We
formulate the following objectives related to a critical system development:

• Establishing a unified theory for the critical systems development.

• Building a comprehensive and integrated suite of tools for the critical systems

that can support verification activities, including formal specification, model val-
idation, real-time animation and automatic code generation.

• Environment modelling for the development of a closed-loop system for verifica-

tion purposes.

• Refinement-based formal development to achieve less error-prone models, easier

specification for the critical systems and reuse of such specification for further
designs.

• Model-based development and component-based design frameworks.

• System integration of critical infrastructure. Possibility of annotating models for

different purposes, (e.g., directing the synthesis or hooking to verification tools).

• Evidence-based certification through animation.

• Requirements and metrics for certifiable assurance and safety.

The enumerated objectives are covered in this topic through developing a new
development life-cycle methodology and a set of associated techniques and tools
for developing the critical systems. The development life-cycle methodology is a
development process for the systems to capture the essential features precisely in
an intuitive manner. A development methodology including a set of techniques and
tools is developed for handling the stakeholders requirements, refinement-based sys-
tem specification, verification, model animation using real-time data set through a
real-time animator, and finally automatic source code generation from the verified
formal specification to implement a system.
The formal verification and model validation offers to meet the challenge of
complying with FDA's QSR, ISO, IEEE, CC [ 6 , 8 , 12 , 13 ] quality system direc-
tives. According to the FDA QSR, validation is the “confirmation by examination
and provision of objective evidence that the particular requirements for a specific