Critical System Development Methodology - Using Event-B for Critical Device Software Systems - page 61

techniques than the other large systems like imaging for diagnostics or surgery nav-
igation, patient monitoring system, etc.
Software is an essential part of any critical system, which realises system's func-
tionality and software reliability for gaining confidence. From the last few years,
the use of critical systems has been increased [ 69 ]. These devices may sometimes
malfunction. Device-related problems are responsible for many accidents. A lot of
deaths and injuries have been reported by the US Food and Drug Administration's
(FDA) caused by failure of medical devices [ 51 ], which advocate safety and secu-
rity issues for using it. Certification standards have found that many accidents due
to system failure, are caused by product design and engineering flaws, which are
considered as the firmware problems [ 16 , 28 ].
Manufacturers have the freedom to tailor the process and to select appropriate
methodology according to their specific needs. A lack of information about pro-
cess and product qualities leads to uncertainness about the appropriateness of the
methodology. Software development measures both processes in the quality man-
agement plan and associated safety cases related to the approval of the products.
Formal methods are usually applied for analysing assumptions, relationships, and
requirements of the system.
Software certification is performed by certification standards, like FDA, IEC/ISO,
IEEE [ 35 , 36 , 43 ], which do not prove the correctness of a system. If a product re-
ceives certification, it simply means that it has met all the requirements needed for
certification. It does not mean that the product is bug-free . Therefore, the manu-
facturer cannot use certification to avoid assuming its legal or moral obligations.
Many standards consist of functional requirements on the particular medical prod-
ucts; there are also a number of standards, which address system safety and software
development. For example, IEC-62304 [ 34 ] process standard for the quality and risk
management of medical devices.
The scope of formal methods is limited in the current industrial practices, which
address that the formal methods are not well integrated into established critical sys-
tem development processes. Formal methods need high abstraction and mathemat-
ical skills to write specifications and conduct proofs, and to read and understand
formal specifications and proofs, especially when they are complex, are the main
reasons for not using in practices. Another important cause is that existing formal
methods do not offer usable and effective methods to employ in the well-established
industrial software process. None of the existing tools are able to support the formal
techniques based software-development, although tools are supporting the use of
formal methods in limited areas are available in [ 41 , 45 , 59 ]. To make formal meth-
ods more practicable and acceptable in industry, some substantial changes must be
made.
Although formal methods are part of the standard recommendations [ 28 ] for de-
veloping and certifying the critical systems, how to integrate formal methods into
the certification process is, in large part, unclear. Especially, it is challenging that
how to demonstrate the final developed system that behaves safely. This chapter
describes formal methods based development process that we have applied to pro-
duce evidence for the certification, based on the certification standards [ 15 , 23 , 36 ],