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

formal methods to apply in the system development process. Increasingly, number
of successful development of techniques and tools related to the formal methods,
the industries have started to adopt it for verifying the safety properties of complex
systems [ 13 , 14 , 23 , 97 ]. For verifying a critical system, industries prefer to use for-
mal methods-based techniques such as model checking or theorem proving in place
of the traditional simulation techniques. In both areas related to the model check-
ing and theorem proving, the researchers and practitioners are performing more and
more industrial-sized case studies [ 9 , 11 , 13 , 24 , 38 , 61 , 62 , 78 ], and thereby gaining
the benefits of using formal methods.
This chapter briefly discusses safety critical systems, examines the use of for-
mal techniques to provide safety and reliability, analysis the use of traditional safety
techniques for software, surveys on regulations for medical devices, and gives a
list of successful industrial case studies based on formal techniques. Reliability and
safety are the most important attributes of critical systems. The main objective of
this chapter is to provide information about current safety issues in medical do-
main particularly for the safety critical software systems. It should be noted that the
formal methods are the most important techniques that are applicable for a safety
related software development for medical devices using several classical safety anal-
ysis techniques.
2.1.1 Structure of This Chapter
This chapter contains a concise survey that reviews the existing literatures relating
to the development and analysis of a software for safety critical systems, which
identifies current valuable approaches for developing the safety critical software,
and reviews the methods and analysis techniques available to the system develop-
ers. Section 2.2 gives an overview about reliability and safety. Section 2.3 presents a
role of a software in safety-critical systems and Sect. 2.4 describes safety life-cycle
for critical systems. Section 2.5 presents traditional safety analysis techniques. Sec-
tion 2.6 explores the traditional system engineering approach, and Sect. 2.7 gives
a list of standard design methodologies for the system development process. Sec-
tion 2.8 depicts about safety standards, and Sect. 2.9 presents medical device stan-
dards and discusses the current issues of regulations. Section 2.10 presents a list of
industrial projects related to the formal methods, and finally, Sect. 2.11 discusses
the use of formal methods for the safety critical software systems.
2.2 Reliability and Safety
2.2.1 Reliability
Reliability is a fundamental attribute for the safe operation of any critical system.
According to the Institute of Electrical and Electronic Engineers (IEEE), “ Reliabil-
ity is the ability of a system or component to perform its required functions under