Formal safety analysis techniques compute all minimal critical fault sets of safety-critical systems. These sets represent combinations of faults that can cause safety hazards, i.e., situations resulting in environmental damage, injuries, or loss of lives. Deductive Cause Consequence Analysis (DCCA) is one of these techniques, based on [model checking](Model Checking), that rigorously determines the relationships between faults (the causes) and hazards (the consequences). DCCAs are conducted automatically by S#.

Be sure to understand S#'s [model life-cycle](Model Life-Cycle) before continuing.

The following is a short, high-level introduction to DCCA. The details are not important for working with S#, as S# conducts DCCAs fully transparently for the user. For a more detailed and more formal introduction to DCCA, please take a look at our publications.

By model checking a series of formulas, DCCA uncovers cause consequence relationships between faults (the causes) and hazards (the consequences): For each hazard, DCCA computes all minimal critical fault sets that can cause the occurrence of the hazard. In the following, we assume a finite Kripke structure K representing the system to be analyzed with a hazard H given as a propositional logic formula over K not referencing any of K's faults.

A fault set F is critical for a hazard H if and only if there is the possibility that H occurs and before that, at most the faults in F have been [activated](Fault Modeling). Actual activation is only (implicitly) required for minimal criticality, but not for criticality: For any critical fault set F, any super set F' is also critical because additional fault activations cannot be expected to improve safety. In practice, the criticality property's monotonicity with respect to set inclusion often allows for significant reductions in the number of checks required to find all minimal critical fault sets; otherwise, all combinations of faults would have to be checked for criticality. In the worst case, however, DCCA does indeed have exponential complexity.

DCCA determines all minimal critical fault sets for a hazard; it is a complete safety analysis technique in the sense that the hazard cannot occur as long as at least one fault of each minimal critical fault set is never activated.

For the [pressure tank running example](Pressure Tank Case Study), for instance, a DCCA can be conducted as follows:

// 1
var model = new Model();

// 2; important: do not write 'var hazard = ...' as that would evaluate the
// formula immediately
Formula hazard = model.Tank.TankRupture;

// 3
var result = SafetyAnalysis.AnalyzeHazard(model, hazard);

// 4
result.SaveCounterExamples("counter examples");

// 5
Console.WriteLine(result);

1. The first line initializes the model that should be analyzed. In this case, there are no constructor parameters; generally, though, model can be parameterized to allow for different model configurations in order to combine and check various design alternatives of a safety-critical system.

2. Hazards are Formula instances. It is absolutely imperative to declare the hazard variable to be of type Formula. If you use bool or var instead, the formula is evaluated immediately and the model checker checks the resulting constant.

3. The method SafetyAnalysis.AnalyzeHazard(Model, Formula) computes all minimal critical fault sets for the given model and hazard.

Optionally, the maxCardinality parameter (not shown in the example above) can be used to restrict the maximum cardinality of the fault sets that should be checked for criticality. For instance, a value of 1 checks only the empty set and all singleton fault sets for criticality. This is useful if there are many large minimal critical sets: They might not have a large impact on the safety of the system, but will take a while to be found.

If maxCardinality is given, DCCA might not be complete, i.e., not all minimal critical fault sets might be found. result.IsComplete can be used to determine whether a DCCA is definitely complete despite maxCardinality being explicitly specified.

4. For all minimal critical fault sets, the model checker generates a counter example that shows how the faults can cause the occurrence of the hazard. The counter examples can be obtained using result.CounterExamples or saved to disk using the result.SaveCounterExamples(string directory) method.

5. The result object provides programmatic access to all analysis results. Alternatively, a summary of the DCCA results can be output to the console. For the pressure tank case study, the summary looks as follows:

=======================================================================
=======      Deductive Cause Consequence Analysis: Results      =======
=======================================================================

Elapsed Time: 00:00:02.1703065
Fault Count: 4
Faults: SuppressIsEmpty, SuppressIsFull, SuppressPumping, SuppressTimeout

Checked Fault Sets: 13 (81% of all fault sets)
Minimal Critical Sets: 1

   (1) { SuppressIsFull, SuppressTimeout }

The summary shows the total number of faults that were checked, including the names of those faults. Most importantly, it gives the total number of minimal critical sets that were found and the faults they contain. It is also shown how many fault sets had to be checked in order to find all critical ones; for the pressure tank, 81% of all fault sets had to be checked, so the monotonicity of the criticality property did not help much in this case.

Further examples for conducting safety analyses with S# can be found in the case study projects.