4. UseAny SFTA must be preceded by a hazard analysis of the entire system. The information in the hazard analysis identifies those undesired events in the system that can cause serious consequences. It should be noted that in complex systems not all hazards can be predetermined. In this respect the technique does not claim to produce consistent results irrespective of the analyst. It is dependent on the judgment of the individual as to when to stop the process and which hazards to analyze. The SFTA can be used at different stages of the software life cycle. The earliest stage where the technique should be used is Preliminary Design (if, at this point, the design still has excessive TBDs, then the technique is ineffective). In practice it will be used most frequently at the code level, preferably prior to integration and test. The basic procedure in an SFTA is to assume that the hazard has occurred and then to determine its set of possible causes. The technique is useless if one starts with the overly generalized hazard "system fails". A more specific failure, such as those identified from the earlier hazard analysis, has to be the starting point for the analysis. The hazard is the root of the fault tree and its leaves are the necessary preconditions for the hazard to occur. These preconditions are listed in the fault tree and connected to the root of the tree via a logical AND or logical OR of the preconditions (see Figure 2: Example of High Level Fault Tree). In turn, each one of the preconditions is expanded in the same fashion as the root fault (we identify the causes of each precondition). The expansion continues until all leaves describe events of computable probability or the event cannot be analyzed further. The analysis also stops when the precondition is a hardware malfunction that has no dependency on software. The fault tree is expanded from the specified system level failure to the software interface level where we have identified the software outputs or lack of them that can adversely affect system operation. At this stage the analysis begins to take into account the behavior specific to the language. The language constructs can be transformed into templates using preconditions, postconditions and logical connectives. (For templates of Ada constructs, see Leveson et al. [3].) All the critical code must be traced until all conditions are identified as true or false or an input statement is reached. The technique will be illustrated with an example using a Pascal like language [2]. The code will be analyzed for the occurrence of the variable Z being output with a value greater than 100. We should assume B, X, Z are integers. While B>Xdo begin B :=B? 1; Z := Z + 10; end if Z ~ 100 then output Z;
In this piece of code there are assignment statements, an "if" and a "while" construct. The templates for these statements will be applied, starting from the occurrence of the event we are searching for "output Z with Z > 100". Refer to Figure 3: Example Code Fault Tree for the discussion that follows. The templates for the constructs will be drawn showing all the considerations that are required for the analysis to be complete. Some leaves of the tree are not expanded further because they are not relevant to the event or postcondition that we are analyzing. The "if" template shows that the event is triggered by the "then" clause. This follows from the condition in the "if" statement. At this point we need to determine the preconditions necessary for Z > 100 prior to the entry into the while construct. In this example we have only two simple assignments within the "while" construct but they could be replaced by more complex expressions. The analysis would still be similar to that shown here in the example. The "while" construct would be analyzed as a unit and the expressions within the "while" would generate a more complex tree structure as previously described using the language templates to determine the preconditions. By analysis of the transformations in the "while" loop, we arrive at the conclusion that for the Z > 100 to be output, the weakest precondition at the beginning of the code was that for B > X, Z + 1 OB ? 10X > 100. At this point we have identified the weakest condition necessary for this code to output Z with Z > 100. More detailed examples are provided in references [1] and [2]. Anyone interested in applying the technique should study the examples in the two references or other articles where the technique is illustrated. The analysis that was shown in the section above determined the preconditions for the event to occur. One way to preclude a hazard from happening is to place an assertion in the code that verifies that the precondition for the hazard, as determined in the analysis, does not occur. SFTAs point out where to place assertions and the precondition to assert. If the preconditions do occur, some corrective action needs to take place to remedy the problem or, if a remedy is not possible, to mitigate the consequences. Typically, a small percentage of the total software effort on projects will be spent on safety critical code. The Canadian Nuclear Power Plant safety?critical shutdown software was reviewed via the SFTA technique in three work months. The cost of this technique is insignificant considering the total amount spent on testing and verification. Full functional verification of the same software took 30 work years [3]. In cases where no problems are found, the benefits can still justify the investment. The resulting code is made more robust by the inclusion of the safety assertions and the analysis verifies that major hazardous states identified have been avoided. Due to complexity, the figures from the example cited above (3 work months for 6K lines of code) will probably not scale up. The technique can be selectively applied to address only certain classes of faults in the case where a large body of safety critical code requires a safety verification. |