基于 HOL 定理证明的洗牌交换网络动态可靠性分析
计算机科学中的逻辑
2019-10-25 v1
摘要
动态可靠性模型，如动态故障树 (DFTs) 与动态可靠性框图 (DRBDs)，被引入以克服传统模型的建模局限。近来，这两种模型的高阶逻辑 (HOL) 形式化已完成，从而可在定理证明器内对这些模型进行形式化分析。在本报告中，我们对洗牌交换网络——一种常用于多处理器系统的多级互连网络——提供形式化动态可靠性分析。我们使用 DFTs 与 DRBDs，借助动态备件门与构造的若干通用版本对终端、广播与网络可靠性建模。我们验证了这些系统失效概率与可靠性的通用表达式，其可用任意数量的系统组件与失效率实例化，以推理这些网络的失效行为。
引用
@article{arxiv.1910.11203,
title = {Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving},
author = {Yassmeen Elderhalli and Osman Hasan and Sofiene Tahar},
journal= {arXiv preprint arXiv:1910.11203},
year = {2019}
}