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

Mainly, four traditional models of software evolution are very popular from the
earliest days of software engineering. These four models are waterfall model, step-
wise refinement model, incremental release model and military standards based
model. The most familiar software-development model is the waterfall model,
which was originated by Royce [ 60 ]. This model presents a way for develop-
ing a large complex software system using an iterative process. Stepwise refine-
ment model develops the software system through the progressive refinement and
helps in enhancement of the high-level system specifications into source code
components [ 56 , 68 ]. The refinement process is undefined, while it is used dur-
ing the development process, and formalisation is expected to apply heuristically
according to the expertise and acquired skills. These two models are effective
and widely applied in the current practices of the software engineering [ 52 ]. The
incremental release model is mostly applied into industrial practices. Develop-
ing systems through incremental release provides a foundation level for essen-
tial operating functions, then enriching the system functionalities at the regular
intervals [ 5 ]. This model combines the classic software life-cycle with an iter-
ative enhancement at the level of system development organisation. Periodical
software maintenance and services are also supported by this incremental release
model.
Military standards based models are the refined form of the classical life-cycle
models, which eliminate complications that emerge during large software develop-
ment. Since 1970's many government contractors use military standards for devel-
oping the large software systems [ 20 ]. Military software system is not commonly
used in the industrial and academic practices. Mainly, it is used for: (1) meeting
required military standards; (2) developing complex embedded systems (e.g., air-
planes, submarines, missiles, command and control systems), which are mission-
critical; and (3) developing under contract to private firms through cumbersome
procurement and acquisition procedures that can be subject to public scrutiny and
legislative intervention [ 20 ].
All these four models are used for coarse-grain characterisations of the software
evolution. The primary progressive steps of software evolution are requirements
specification, design, and implementation. Moreover, these models are independent
of any organisational development setting, software application domain, choice of
programming language, etc. However, all of these life-cycle models have been in
use for some time, we refer to them as the traditional models, which are used for
software evolution [ 52 ].
There have been several efforts involving the use of formal methods to verify
safety-critical systems. Formal methods have been used to handle complex safety-
critical systems, for instance, steam boiler control [ 2 ], Siemens Transportation Sys-
tems [ 4 ], space and avionic system [ 13 , 18 , 25 , 42 , 57 ] and so on. Various for-
malisms and rigorous techniques (VDM [ 9 ], Z [ 66 ], ASTRÉE [ 18 ], SCADE [ 7 ],
Event-B [ 1 ], Alloy [ 37 ], CSP [ 29 ], PVS [ 19 ], SPIN [ 30 ], etc.) have been used for
developing the safety-critical systems. These approaches provide a given level of
reliability and confidence to develop an error-free system. Few case studies show