Compositionality of Component Fault Trees

摘要

In order to deal with the rising complexity of safety-critical systems, model-based systems engineering (MBSE) approaches are becoming popular due to their promise to improve consistency between different views of the system model. Component Fault Trees (CFTs) are one particular technique to integrate the well-known Fault Tree Analysis (FTA) with a model of the system. CFTs decompose the specification of fault propagation on component level, which results in smaller, easier to manage models and leads to a safety analysis view that is consistent with the system model. However, although CFTs gain more and more popularity, their semantics is not well defined and the compositionality of CFTs is not formally proven to the best of our knowledge. In this paper, we provide a formal basis for CFTs, formalize semantics of CFTs and formally prove compositionality of CFTs by mapping them to information flow semantics, which is well-researched in the security analysis domain. Our results allow insights in the compositionality of CFTs, showing a high potential for validation techniques of CFTs and discuss these consequences in detail. We claim that this proof is crucial for the use of CFTs in assurance cases for safety-critical systems and one fundamental approach to integrate safety and security engineering.