Developer

Safety-critical projects: Can formal methods help?

Vague, contradictory, or incomplete software specifications can cause disastrous system failure. A math-based formal specification method will eliminate flaws that can lead to failure in safety-critical systems.


When the failure of a computer system can lead to catastrophic consequences, such as the loss of human life, damage to the environment, or damage to the system itself, such a system is known as “safety-critical.” In the past 20 years, there have been approximately 1,100 computer-related accidental deaths. Obviously it’s of the utmost importance to specify safe and reliable software in safety-critical systems.

The aim of requirements analysis is to get a precise and independent description of a future software system. The normal approach is to undertake a structured or object-oriented analysis. For specifying safety-critical applications, project managers and systems analysts are turning to formal methods. This math-based technique can assure you that a complete specification has been created for a sensitive application. Formal methods are still being developed for commercial use and remain difficult to deploy effectively.

A specification will include the following main aspects:
  • Information flows
  • Functions used to transform input to output
  • Definition of the interfaces
  • Organization and description of the different levels of representation and abstraction

These have traditionally been written down in long, turgid documents. Such natural language or graphical system specifications suffer from several inherent flaws. I’ll examine these flaws and then discuss how a formal method of specification can help eliminate them.

Contradiction
Contradictory statements in a lengthy specification are often separated by many pages and remain undetected—until your team is knee-deep in coding.

Here is an example: “The system will always operate on values between levels 0.0 and 2.0….” This statement is later contradicted by another: “Module X will be required to read in data from an external source over the range of integer values 0 to 10.”

Ambiguity
Ambiguity is common in written specifications: “The system will read in 120 initial data values and compute the mean and mode. They will be stored for later analysis.”

What exactly must be stored? If raw data is required elsewhere, this doesn't allow for it here.

Vagueness
Most project managers will pick up on any significant imprecision, but sometimes a client will cite a vague part of the specification later, as if it were a guarantee: “The storage requirements should be as small as possible.”

Obviously this is useless in a specification, but the danger is that a project plan might be drawn up before this vagueness is clarified.

Incompleteness
This is the hardest flaw to deal with when working with real users. For example: “The system will accept time entries ranging from 03:00 on 1/2/02.”

But what if someone just enters 02/02/02?

Mixed levels of abstraction
It can be terribly hard to see the overall functional architecture when the levels of description are intermixed, like this: “The system will make it easy to access the values in all consumer accounts. This will involve extraction of the 5-digit real values by clicking on the tab to the left of the rightmost frame on the entry page….”

Formal specification can answer such flaws
People—even IT Project Managers—often have difficulty communicating with each other and especially with their machines. Mathematics is the language of computers, and, unlike natural language, it leaves no room for any of the above uncertainties. It's therefore possible to use mathematics to specify exactly what software needs to do. Math-based formal methods overcome all of the above specification problems, and they also allow validation (i.e., we can prove a design meets a particular specification before any coding occurs).

Formal specification of software involves three main concepts:
  • The Data Invariant: This is a set of rules that governs the range and nature of the data in the system throughout its operation.
  • The State: These are the actual values stored in the system.
  • Operations: These simply read or write data to a State. Each operation has a precondition (i.e., a statement of conditions for the particular action to be allowed to proceed) and a postcondition (i.e., a statement of what happens when the operation is complete).

For example, Z is a language based on the notation of sets for formal specification of industrial software systems. Until recently, it suffered from a lack of tools, such as typecheckers, documentation tools, and appropriate theorem-provers that could automatically validate a formal specification.

Preventing system failure
The three main causes of failure in software systems are physical causes, software errors, and human/computer interference. You can alleviate all of these by using formal specification.

Even in a safety-critical application, software may fail frequently yet still not lead to unsafe behavior. On the other hand, highly reliable software can be unsafe because, in the rare event of a failure, the effect is dangerous.

Ideally, software designers and manufacturers should demonstrate that software specification forbids actions that lead to catastrophic failures of the system. The software should also protect itself from failures of the other parts of the system. The only way to be certain that a system is specified as safe is to rely on formal techniques. This will require you to create more friendly interfaces for project managers and designers who aren't professional mathematicians.

In the future, we may need to use combinations of formal verification, more advanced testing, and other methods to achieve the genuinely safe operation of software-controlled systems.

Editor's Picks

Free Newsletters, In your Inbox