Evaluating the reliability of NAND multiplexing with PRISM
Evaluating the reliability of NAND multiplexing with PRISM
复制标题
DOI：
10.1109/tcad.2005.852033
复制
发表时间：
2005-10-01
影响因子：
2.9
通讯作者：
Shukla, S
中科院分区：
文献类型：
--
作者：
Norman, G;Parker, D;Shukla, S
概率模型检查是一种形式验证技术，用于分析表现出随机行为的系统的可靠性和性能。在本文中，我们证明了这种方法的适用性，特别是概率模型检查工具 PRISM 在计算机辅助设计领域评估容错系统的可靠性和冗余性。我们用冯·诺依曼提出的一个例子来说明该技术，即 NAND 多路复用。我们展示了在构建了包含缺陷概率假设的容错系统模型后，如何直接计算一系列可靠性度量并研究它们如何受到系统行为的微小变化的影响。例如，这允许设计者评估设计中冗余和可靠性之间的权衡。我们还强调了最近针对同一案例研究发表的分析计算可靠性范围中的错误。
Probabilistic-model checking is a formal verification technique for analyzing the reliability and performance of systems exhibiting stochastic behavior. In this paper, we demonstrate the applicability of this approach and, in particular, the probabilistic-model-checking tool PRISM to the evaluation of reliability and redundancy of defect-tolerant systems in the field of computer-aided design. We illustrate the technique with an example due to von Neumann, namely NAND multiplexing. We show how, having constructed a model of a defect-tolerant system incorporating probabilistic assumptions about its defects, it is straightforward to compute a range of reliability measures and investigate how they are affected by slight variations in the behavior of the system. This allows a designer to evaluate, for example, the tradeoff between redundancy and reliability in the design. We also highlight errors in analytically computed reliability bounds, recently published for the same case study.