A verification of fault tree for safety integrity level evaluation

This study focuses on a novel approach which automatically proves the correctness and completeness of fault trees based on a formal model by model checking. This study represents that the model checking technique is useful when validating the correctness of informal safety analysis such as FTA. The benefits of this study are that it provides the probability of formally validating FTA by proving correctness and completeness of the fault trees. In addition to this benefit, it is possible that the CTL technique proves the FTA based SIL.