5 Protecting Against What You Have Forgotten About

It is far easier to protect against what you fear than what you have failed to fear. Formal methods, if properly applied, can do much for the former and little for the latter.

Successfully applying formal methods can, at best, result in software that does precisely what was specified. If the specifications are wrong and certain undesirable output behaviors were accidentally not defined in the specification (and thus not protected against in the code), formal methods will be helpless.

Here, one variation on traditional software testing, software fault injection, can help warn of undesirable capabilities of the software that the specification/requirements have failed to warn against. Although this process will involve manual effort (thus making the process less than foolproof), it can force the software to reveal outputs that were not known to be possible.

Fault injection is a technique that can flush out certain types of undesirable output events after the software is forced to experience certain types of anomalous behaviors [3,2]. To perform fault injection analysis, the user of the technique is required to define the classes of undesirable (or hazardous) output events. Fault injection then observes whether outputs that satisfy these definitions are produced.

Fault injection forces internal states of the software to become corrupted in a variety of ways. These internal corruptions may or may not force the output of the software to be modified. Sometimes the modified output will be instances of what was supposedly deemed as impossible to produce according to the formal analysis. When this occurs, fault injection warns that the software can still produce undesirable outputs that were thought to be impossible. Here, fault injection is testing the development processes just as much as it is testing the code.

Just because an output is produced that was not deemed as undesirable according to the specification does not mean that the output is desirable. After all, the specification defining undesirable output behaviors may be incomplete. Therefore it is valuable to have a person manually sift through those outputs that appear to be acceptable to see if there are any output events that are actually undesirable. If there are, then the specification that defined ``good'' versus ``bad'' output behavior failed to define certain types of outputs as bad. Thus the specification needs to be modified. In this manner, fault injection, in conjunction with manual effort, can analyze the specification for completeness of those definitions that define undesirable behavior.

For an example that brings this back to component-based software engineering, suppose that you have a COTS component that has been ``wrapped'' using formal methods. The formal methods have asserted that certain events from this component are no longer possible. To test this claim, fault injection can force corrupt information into the component, and see what the component does. (Regular testing can be used also.) If we are unable to force the component to exhibit undesirable behaviors, then we can have confidence in the formally-derived wrappers. And if undesirable behaviors are exhibited that were not protected against in the wrapper, then we can use fault injection to define additional wrapping requirements to the wrapper's specification.