4 Protecting Against What You Fear

Ensuring that software only does what you want it to do is a multi-phased process. A good beginning is to define precisely what events you do not want the software to cause. Then it is necessary to design and develop the software such that it cannot cause those events, and finally to demonstrate that the code cannot exhibit those undesirable behaviors.

There are a variety of formal analyses such as fault tree analysis and Petri net analysis that can demonstrate that only ``desirable'' functionality is provided by a software design (and that undesirable functionality is not). Generally speaking, protecting against those events that are feared is a straightforward process: (1) system-level analysis defines those events that must be protected against, and (2) a design technique (like static fault-tree analysis combined with proofs-by-contradiction) mitigates the possibility of those events occurring. If the system includes real-time constraints, formal Petri Net analysis can prove that timing constraints are not violated.

By defining undesirable events early on in the life-cycle, half of the battle of protecting against them is waged. The next task is to actually implement the protection. But even if formal analyses assert that the protection provided in the design and software is adequate, prudence suggests that a real demonstration is needed that executes the software to test the protection.

Experimentation using testing and fault injection are ideal here. These informal analyses provide confidence in the software as well as in the formal analyses. The point here is that the aforementioned informal analyses can measure software quality. Formal methods do not. But a measurement of quality for software that was formally developed is also a measure of process quality. For example, if formal methods say that output event E cannot occur, and the results from testing show that the likelihood of E occurring is less than P, and P is tiny, then testing has effectively substantiated the proposition. In this manner, formal and informal methods can complement each other nicely.