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

intended use can be consistently fulfilled”. Verification is “confirmation by exam-
ination and provision of objective evidence that specified requirements have been
fulfilled” [ 11 , 21 ]. All the proposed approaches may also help to obtain the certifi-
cation standards [ 6 , 8 , 12 , 13 ] in the area of critical system development.
1.2 Approach
In this topic, we present a development life-cycle methodology, a framework for
real-time animator [ 19 ], refinement chart [ 31 ], a set of automatic code genera-
tion tools [ 7 , 18 , 22 ] and formal logic based heart model for closed-loop mod-
elling [ 25 , 29 ]. The development methodology and associated tools are used for
developing a critical system from requirements analysis to code implementation,
where verification and validation tasks are used as intermediate layers for provid-
ing a correct formal model with desired system behaviour at the concrete level. Our
approach of specification and verification is based on the techniques of abstraction
and refinement. Introducing a new set of tools helps to verify the desired proper-
ties, which are hidden at the early stage of the system development. For example,
a real-time animator provides a new way to discover hidden requirements accord-
ing to the stakeholders. It is an efficient technique to use the real-time data set, in
a formal model without generating the source code in any target programming lan-
guage [ 19 ], which also provides a way for domain experts (i.e. medical experts) to
participate in the system development process (medical device development). A ba-
sic description about development methodology and all associated techniques and
tools are provided in the following paragraphs:
We propose a new methodology, which is an extension of the waterfall model [ 3 ,
5 , 34 , 35 ] and utilises rigorous approaches based on formal techniques to produce a
reliable critical system. This methodology combines the refinement approach with
a verification tool, model checker tool, real-time animator and finally generates the
source code using automatic code generation tools. The system development process
is concurrently assessed by the safety assessment approaches [ 15 , 33 , 36 ] to comply
with certification standards [ 6 , 8 , 12 , 13 ]. This life-cycle methodology consists of
seven main phases: first, informal requirements, resulting in a structured version of
the requirements, where each fragment is classified according to a fixed taxonomy.
In the second phase, informal requirements are formalised using a formal modelling
language, with a precise semantics, and enriched with invariants and temporal con-
straints. The third phase consists of refinement-based formal verification to test the
internal consistency and correctness of the specifications. The fourth phase is the
process of determining the degree to which a formal model is an accurate represen-
tation of the real world from the perspective of the intended uses of the model using
a model-checker. The fifth phase is used to animate the formal model with real-time
data set instead of toy-data , and offers a simple way for specifiers to build a domain-
specific visualisation that can be used by domain experts to check whether a formal
specification corresponds to their expectations. The six phase generates the source