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

of a software based critical system. It also describes the most effective aspects of
our methodology for certification and research that could significantly increase the
utility of formal methods in software certification.
The main contribution of this chapter is to propose a development life-cycle
methodology for developing the highly critical software systems using formal tech-
niques from requirements analysis to code implementation using rigorous safety
assessment approach [ 55 ]. This new development life-cycle is an extension of the
waterfall model [ 60 ], which can support formal methods based development using
various tools. In this new development life-cycle, we introduce some new steps,
which are essential for improving the quality of the system. For example, the real-
time animation [ 53 ] helps in requirement traceability and to bridge among various
stakeholders. There are lacks of supporting tools, which can support for developing
critical systems. To realise this new development life-cycle, we use different tech-
niques from the past research related to the field of formal methods and software
engineering. For implementation purpose, we use different tools at various level of
development.
Some new tools, we have developed according to the requirement of this method-
ology like real-time animator [ 53 ], automatic code generation [ 54 ]. There are not
exiting a set of supporting tools, which can be used for developing a system using
formal methods. Our proposed methodology provide a rigorous framework for de-
veloping critical systems, which may give an evidence to obtain certificate from the
international standards [ 15 , 23 , 36 ]. We have applied our proposed approach on an
industrial-scale case study related to the cardiac pacemaker to show the effective-
ness of this new development life-cycle methodology.
4.1.1 Structure of This Chapter
This chapter is organised as follows. Section 4.2 presents related work and Sect. 4.3
describes the heart of the methodology for critical software system development.
Section 4.4 presents benefits of proposed approach. Section 4.5 evaluates this de-
velopment methodology with other existing tools. Finally, Sect. 4.6 summarises this
chapter.
4.2 Related Work
During the 1950's and 1960's [ 31 , 60 ], the main purpose of the software life-cycle
was to provide a conceptual idea for managing the development of software systems.
The conceptual idea was related to the planning, organising, coordinating, staffing,
budgeting and directing the software-development activities. Since the 1960's, dif-
ferent kinds of descriptions and characterisations of the software-development life-
cycle have emerged [ 10 , 21 , 31 , 60 , 62 , 65 ].