Background - Using Event-B for Critical Device Software Systems - page 9

Chapter 2
Background
Abstract Formal methods based system development is considered as a promising
approach to develop the safe critical systems. This chapter discusses the standard
safety life-cycle, traditional safety analysis techniques, traditional system engineer-
ing approach, standard design methodologies and safety standards that are used for
developing the critical systems. Furthermore, we have given a list of successful in-
dustrial case studies based on formal techniques. Moreover, we discuss the role of
medical device regulations. Finally, this chapter shows the usability of formal tech-
niques for developing the critical systems and to motivate for developing a new
methodology, and associated techniques and tool in the context of medical device
development, which are covered in the remaining chapters.
2.1 Introduction
Critical systems are tremendously grown in functionality in both software and hard-
ware, and due to increasingly the complexity of critical systems it is very hard to pre-
dict the absence of failure. Moreover, some of these failures may cause catastrophic
financial loss, time or even human life. One of the main objectives of software engi-
neering is to provide a framework to develop a critical system that operates reliably
despite this complexity. It has been shown in [ 97 , 113 ] that the promising results
are achievable only through the use of formal methods in the development process.
More than a decade, several formal methods based techniques and tools are used by
industries and academic research projects [ 62 , 111 ]. The backbone of formal meth-
ods is considered to be mathematics, which often supports related techniques and
tools based on logico-mathematical theory for specifying and verifying the complex
systems. The techniques and tools based on formal methods provide a certain level
of reliability under some constraints. Formal verification is considered as a bench-
mark technique, particularly in the area of safety critical systems, where important
safety properties are required to prove rigorously before implementing a system.
However, the use of formal methods helps to speculate the hidden peculiarity of a
system like inconsistencies, ambiguities, and incompleteness.
In the past, formal methods based technique was not into practice in the soft-
ware development life-cycle due to the use of complex mathematical notations; in-
adequate tools support and too hard to apply. Special training was required to use