Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving

TL;DR

This paper presents a formal, theorem-proving approach to analyze the dependability of shuffle-exchange networks using dynamic fault trees and reliability block diagrams, enabling generic and scalable reliability assessments.

Contribution

It provides the first formal HOL-based dynamic dependability analysis of shuffle-exchange networks, modeling reliability with dynamic constructs and verifying generic failure probability expressions.

Findings

Verified generic failure and reliability expressions for shuffle-exchange networks.

Demonstrated the applicability of HOL theorem proving to complex network dependability.

Enabled scalable analysis with arbitrary component numbers and failure rates.

Abstract

Dynamic dependability models, such as dynamic fault trees (DFTs) and dynamic reliability block diagrams (DRBDs), are introduced to overcome the modeling limitations of traditional models. Recently, higher-order logic (HOL) formalizations of both models have been conducted, which allow the analysis of these models formally, within a theorem prover. In this report, we provide the formal dynamic dependability analysis of shuffle-exchange networks, which are multistage interconnection networks that are commonly used in multiprocessor systems. We use DFTs and DRBDs to model the terminal, broadcast and network reliability with dynamic spare gates and constructs in several generic versions. We verify generic expressions of probability of failure and reliability of these systems, which can be instantiated with any number of system components and failure rates to reason about the failure behavior of these networks.