Dynamic dependability analysis of shuffle-exchange networks

Designing dependable multiprocessor systems requires reliable interconnection networks. Multistage interconnection networks (MINs), including shuffle-exchange networks (SENs), are widely used to establish the desired connection. The failure of these networks can degrade the overall system performance, which may lead to significant losses. In this paper, we propose to formally model and analyze the dynamic dependability aspects of SENs using a combination of dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs) based on higher-order logic (HOL) theorem proving. We propose to integrate these two modeling approaches for efficiently handling the considered formal dependability analysis by leveraging upon the advantages of each method. The soundness of this integration is provided through a formal proof of equivalence between the DFT and DRBD algebras. We utilize the proposed framework to provide the formal DFT and DRBD analyses of three common measures of SENs, namely: terminal, broadcast and network reliability. The proposed approach allowed us to verify generic expressions of probability of failure and reliability of these systems, which can be instantiated with any number of system components and time-to-failure functions.