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

2.11 Formal Methods for Safety-Critical Systems
This section presents the use of formal methods in the critical device system soft-
ware development through providing some informal definitions of the main con-
cepts.
2.11.1 Why Formal Methods?
Providing a high integrity system with the embedded software requires a careful ar-
gument for its justification. Demonstrating the requirements through sufficient sta-
tistical evidence based on testing, and other general reliability measures has been
shown to be doubtful. Thus, some other kinds of arguments have to be written,
which must be precise—in language that is well-defined, whose meaning is clear,
and with the ability to prove statements without doubt. Since natural language is
unable to fulfil such demands, the only possible solution is to use a mathematical
approach—formal methods [ 103 ].
A formal approach is an ideal for verification, the activity guaranteeing correct-
ness, that we are building the system right and particularly, that successive refine-
ments of a specification are consistent with each other. More than that, the discipline
which they encourage often leads to a more careful analysis of the most basic as-
sumptions and definitions in the design, a benefit which is often understated [ 103 ].
In particular, they may point to ambiguities in the requirements' definition. Formal
methods are thus effective for validation—making sure that we are building the right
system [ 13 , 47 , 102 ].
The main objective of formal methods is to help developers to build the reliable
systems. Formal methods is a cutting-edge technology for developing the critical
systems, where high safety and security are required. Mathematics is a basic foun-
dation for formal logic that provides some ways to discover potential errors at the
early stage of the development. Figure 2.8 presents modified V-model after intro-
ducing formal methods in a development process. This figure shows that module
testing and integration testing are not required due to formally verified system at
the specification and design level. Formal methods help to reduce the burden of ex-
haustive testing, which are used by the traditional development. Formal techniques
verify the whole system at the early stage of the system development during speci-
fication and design, and to prove the correctness of the system. We cannot say that
formal method is a silver bullet, but it is more reliable than the other traditional de-
velopment approaches. Now formal methods' techniques are feasible to apply for
any larger and complex problems.
2.11.2 Motivation for Their Use
The use of formal methods is very limited in current industrial practice. It is mainly
used for verification and validation of any specific part of the system. Specifically,