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

2.10 Industrial Application of Formal Methods
This section surveys previous works related to the critical system development.
A common theme in much of this work is to use formal methods. Formal methods
provide numerous tools and techniques for solving the different kinds of problems.
Mainly formal methods are applicable for verification and validation of a system.
Formal methods are used to verifying the specification of a system. Although the
safety-critical systems have got the confidence in the development due to use of for-
mal methods, such techniques are applicable in a wide variety of application areas
in industry. Formal methods have been used to improve the quality of the system as
well as verifying the correctness of a system at an early stage of the system develop-
ment. A set of examples that pioneered the application of formal methods, to more
recent examples that illustrate the current state of the art. Here, we have given a
list of industrial applications, where formal methods have been used in the projects.
A detail survey of all these projects is presented in [ 13 , 14 , 23 , 97 ].
2.10.1 IBM's Customer Information Control System
A successful application of formal methods was the verification of the Customer In-
formation Control System (CICS) in 1980, which was collaborated between Oxford
University and IBM Hursley Laboratories [ 49 ]. The overall system contains more
than 750,000 lines of code. Some part of the code was produced from Z specifica-
tions, or partially specified in Z, and the resulting specifications were verified using a
rigorous approach. Some tools, related to the type checking and parsing were devel-
oped during the project, which were used to assist the specifier and code inspector.
More than 2000 pages of formal specifications were developed for verifying the sys-
tem. Measurements taken by IBM throughout the development process indicated an
overall improvement in the quality of the product, a reduction in the number of errors
discovered, and earlier detection of errors found in the process [ 23 ]. Furthermore, it
was estimated that the use of formal methods reduced 9 % of the development cost
for the new release of the software.
2.10.2 The Central Control Function Display Information System
(CDIS)
The Center Control Function Display (CDIS) System was delivered from Praxis to
the UK Civil Aviation Authority in 1992 for London's airspace as a new air traffic
management system [ 39 ]. The CDIS system consists of fault tolerant architecture of
a distributed network, where more than 100 computers are linked together. Formal
methods were used at various levels of the system development. The requirements
analysis phase was represented by formal descriptions using structured notations.