Ada95 Lovelace Tutorial Section 17.4 - Safety and Ada
Section 17.4 - Safety and Ada
While Ada is used in applications where safety isn't a
significant concern,
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
[Gowen 1994].
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
comp.risks
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.
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
first made.
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.
Leveson [1983]
provides a general discussion on software FTA, while
Leveson [1991b]
shows specifically how to apply software FTA to
Ada programs.
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
program properties.
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
over time.
The
Internet directory YAHOO has several references to
information relating to formal methods.
Well-known specification languages include VDM and
Z
(pronounced "zed").
Ada is often used in safety-critical software because of its built-in
capabilities.
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
range.
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
('Valid
is explained in RM 13.9.2).
The expression
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).
Pragma
Restrictions (see RM 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
"Safety and
Security" annex
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.
Using SPARK,
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.
More
information about SPARK is available on the WWW.
Pyle [1991]
discusses and compares various restrictions for safety purposes in his book.
Quiz:
Go back to the previous section
Skip to the next section
Go up to lesson 17 outline