Explain when it may be cost-effective to use formal specification and verification in the development of safety-critical software systems. Why do you think that critical systems engineers are against the use of formal methods?

Question

What will be an ideal response?

Answer 1

Formal methods can be cost-effective in the development of safety-critical software
systems because the costs of system failure are very high and so additional cost in
the development process is justified. Most safety-critical systems have to gain
regulatory approval before they are used and it is a very expensive process to
convince a regulator that a system is safe. The use of a formal specification and
associated correctness argument may be less than the costs e.g. of additional testing
to convince the regulator of the safety of the system.
Some developers of systems are against the use of formal methods because
they are unfamiliar with the technology and unconvinced that a formal
specification can be complete representation of the system. Furthermore, the
problem with formal specifications are that they cannot be understood by system
customers so they may conceal errors and give a false picture of the correctness of
the system.