Page 353 -

336 Chapter 12 Dependability and security specification

Formal specification costs

Developing a formal specification is an expensive process as quite a lot of time is needed to translate the
requirements into a formal language and check the specification. Experience has shown that savings can be
made in system testing and verification and it seems that specifying a system formally does not significantly
increase the overall development costs. However, the balance of costs changes, with more costs incurred early
in the development process.
http://www.SoftwareEngineering-9.com/Web/FormalSpecCosts/

3. Most software engineers have not been trained to use formal specification lan-
guages. Hence, they are reluctant to propose their use in development processes.
4. It is difficult to scale current approaches to formal specification up to very large
systems. When formal specification is used, it is mostly for specifying critical
kernel software rather than complete systems.
5. Formal specification is not compatible with agile methods of development.

Nevertheless, at the time of writing, formal methods have been used in the devel-
opment of a number of safety- and security-critical applications. They may also be
used cost effectively in the development and validation of critical parts of a larger,
more complex software system (Badeau and Amelot, 2005; Hall, 1996; Hall and
Chapman, 2002; Miller et al., 2005; Wordworth, 1996). They are the basis of tools
used in static verification such as the driver verification system used by Microsoft
(Ball et al., 2004; Ball et al., 2006) and the SPARK/Ada language (Barnes, 2003) for
critical systems engineering.

KEY POINTS

Risk analysis is an important activity in the specification of security and dependability
requirements. It involves identifying risks that can result in accidents or incidents. System
requirements are then generated to ensure that these risks do not occur and, if they do, that
they do not lead to an incident or accident.
A hazard-driven approach may be used to understand the safety requirements for a system. You
identify potential hazards and decompose these (using methods such as fault tree analysis) to
discover their root causes. You then specify requirements to avoid or recover from these problems.

Reliability requirements can be defined quantitatively in the system requirements specification.
Reliability metrics include probability of failure on demand (POFOD), rate of occurrence of
failure (ROCOF), and availability (AVAIL).