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.

Some good survey papers that give an overview of the software safety field include Place [1993], Leveson [1991a], and Leveson [1986], Note that [Place 1993] 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:

  1. 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.
  2. 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").

One web server on safety is the 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 capabilities. Here are some Ada capabilities specifically for safety-critical systems:

  1. 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.
  2. 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.
  3. 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:

  1. 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.
  2. Pyle [1991] discusses and compares various restrictions for safety purposes in his book.

Quiz:

Given the following two statements:

  1. If a program is reliable and has been extensively tested, it's safe.
  2. The safety implications of software can be analyzed by itself, without examining how the software will be used.

Which is true?

  1. Statement 1.
  2. Statement 2.
  3. Both statement one and statement two.
  4. Neither statement.

You may also:

PREVIOUS Go back to the previous section

NEXT     Skip to the next section

OUTLINE  Go up to lesson 17 outline

David A. Wheeler (dwheeler@dwheeler.com)

The master copy of this file is at "http://www.adahome.com/Tutorials/Lovelace/s17s4.htm".