Towards tensor-based reliability analysisof complex safety-critical systems
Dániel Szekeres · Zenodo (CERN European Organization for Nuclear Research) · 2021
The failure of complex safety-critical cyber-physical systems can endanger human lives, or cause a high amount of financial loss. Throughout the development of such systems, taking extra-functional requirements - like safety, reliability and performance - into account is of utmost importance. These kinds of requirements are mostly quantitative, meaning that they give target values for some metrics of the system that must be achieved. Achieving these values must be assured already in the design phase, when no usable instance of the system under development is available for measurement, only a model describing its behavior. The reliability and availability metrics are derived using a stochastic model explicitly describing the randomness inherent in the behavior of the system. In my work, I focus on a widely used stochastic modeling formalism called fault trees. This formalism is based on the decomposition of the system-level error: it describes the system-level error as a logic function of the error of the system's elementary components. To calculate the necessary metrics from the model, like mean time to first failure, a lower level analysis model must be derived from it, that can be handled mathematically. When creating and analyzing this low-level model, the problem of state-space explosion arises: even though the high-level engineering model is of tractable size, the size of the corresponding analysis model is exponential in the original one's size. Because of this, the scalability of widespread explicit analysis methods is limited. A possible solution to this problem is storing the linear equation system that needs to be solved during the analysis in a concise approximate form using tensor representation methods, and seeking the solution in the same format. I examined the applicability of Tensor Train (TT) methods for fault tree in my work. I use decision diagram-based state space representation for the derivation of the compressed form, which is widely used in symbolic model checking. There are several different iterative algorithms for solving equation systems in the TT format to perform the necessary calculations. Throughout my work I compare and extend these methods for the solution of problems arising in the analysis of fault trees. I verify the correctness of the theoretical results through measurements performed on large fault trees, using not just the iterative TT algorithm, but widely used explicit methods as well.