Section 17.4 - Safety and Ada
While Ada is used in applications where safety isn't a
many safety-critical applications are developed in Ada.
Even if you're not planning to build safety-critical software
today, it's good to know some basics.
First we'll introduce some software safety concepts, then
follow them with Ada-specific items.
Software Safety Overview
Software safety involves ensuring that software executes within a
system context without resulting in an unacceptable system risk. Safety
is a property of an entire system, not just software, but software
components can be a determiner of a system's safety.
Risk may be defined as a function of (1) the probability of a mishap and
(2) the severity of a mishap's effects should the mishap occur.
Few things in real life can be "perfectly" safe; instead, we try to reduce
the risk to some very small, acceptable level.
One common misconception is that a well-tested, highly reliable
software system is safe. It has been demonstrated experimentally that
traditional verification (testing) techniques are grossly inadequate for
detecting safety-critical faults even for a simple program
Thus, simply testing a system is unlikely to result in a safe system.
A reliable system isn't necessarily a safe system either; a
system that works most of the time but occasionally kills everyone
in a large radius would usually be considered unsafe.
The moderated newsgroup
provides a continuous stream of examples of
software going awry and causing serious problems.
Personally, I think that if you're developing software that could
cause death, serious injury, or significant property damage, you
should be just a little afraid.
If you aren't, you probably
don't understand the issues involved.
That small amount of fear is healthy, because it will motivate you
to learn and use techniques to reduce the overall risk.
Some good survey papers that give an overview of the software safety
is freely available through the Internet.
There are a number of specialized hazard analysis techniques that help to
identify safety problems.
Here are two of them:
- Software Fault Tree Analysis (FTA)
is a technique for identifying potential causes of safety
hazards in a system.
In software FTA, a list of safety hazards (conditions to be avoided) is
Then the analyst assumes that, for analysis purposes,
that each hazard (in turn) has occurred.
The analyst then works
backwards from those hazards through the software,
creating logic diagrams, to show that how the safety hazards can occur
(ideally, the analyst should determine that they cannot occur).
The technique is easy to understand and can be easily integrated
with system safety work.
provides a general discussion on software FTA, while
shows specifically how to apply software FTA to
- Another set of safety-related techniques are
called formal methods.
Formal methods are the application
of (formal) mathematical techniques for definition and possibly proof of
Currently formal methods are a subject of a great deal of research,
but they are not often used in practice due to the difficulty of
applying them to realistic program sizes.
Still, there are systems which have used formal methods to varying degrees,
and there is reason to hope that their applicability will increase
Internet directory YAHOO has several references to
information relating to formal methods.
Well-known specification languages include VDM and
One web server on safety is the
World Wide Web Virtual Library: Safety-Critical Systems.
This web server emphasizes the formal methods aspects, but does cover
others to some extent.
Ada and Software Safety
Ada is often used in safety-critical software because of its built-in
Here are some Ada capabilities specifically for safety-critical systems:
- In some circumstances it's important to check to see if a scalar
value (such as an Integer or enumerated type) is in a legal
For example, hardware errors and cosmic rays can cause values to change
outside of software control, and foreign language interfaces can pass
in out-of-range values.
Ada 95 has an attribute named 'Valid to check if a value is out-of-range
is explained in LRM 13.9.2).
X'Valid, where X is some scalar variable, is True if X is in-range
and False otherwise.
- In safety systems the computer language is often restricted to constructs
that are easier to show correct (either for formal methods or just to
avoid potential problems).
Restrictions (see LRM 13.12)
can be used to specify what parts of the language
may not be used in a particular program.
- Ada 95 has an optional
which, if implemented in the compiler, adds additional operations and features
to support safe and/or secure program development.
For example, this annex adds pragma Normalize_Scalars, which sets
uninitialized values to out-of-range values where possible (this makes
it easier to detect uninitialized values).
Here are two examples of safety-restricted Ada subsets:
- SPARK is a `safe' subset of Ada 83 designed to be
susceptible to formal methods, accompanied with a set of approaches and tools.
a developer takes a Z specification and performs a stepwise
refinement from the specification to SPARK code. For each refinement
step a tool is used to produce verification conditions (VC's), which are
mathematical theorems. If the VC's can be proved then the refinement
step will be known to be valid. However if the VC's cannot be proved
then the refinement step may be erroneous.
information about SPARK is available on the WWW.
- Pyle 
discusses and compares various restrictions for safety purposes in his book.
Given the following two statements:
- If a program is reliable and has been extensively tested, it's safe.
- The safety implications of software can be analyzed by itself,
without examining how the software will be used.
Which is true?
- Statement 1.
- Statement 2.
- Both statement one and statement two.
- Neither statement.
You may also:
David A. Wheeler (firstname.lastname@example.org)