Evaluating the reliability of NAND multiplexing with PRISM
- 26 September 2005
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
- Vol. 24 (10) , 1629-1637
- https://doi.org/10.1109/tcad.2005.852033
Abstract
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.Keywords
This publication has 20 references indexed in Scilit:
- Controller dependability analysis by probabilistic model checkingControl Engineering Practice, 2007
- Probabilistic symbolic model checking with PRISM: a hybrid approachInternational Journal on Software Tools for Technology Transfer, 2004
- Performance Analysis of Probabilistic Timed Automata Using Digital ClocksPublished by Springer Nature ,2004
- Symbolic Model Checking for Probabilistic Timed AutomataPublished by Springer Nature ,2004
- Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention ProtocolFormal Aspects of Computing, 2003
- A system architecture solution for unreliable nanoelectronic devicesIEEE Transactions on Nanotechnology, 2002
- A Defect-Tolerant Computer Architecture: Opportunities for NanotechnologyScience, 1998
- On the maximum tolerable noise for reliable computation by formulasIEEE Transactions on Information Theory, 1998
- A logic for reasoning about time and reliabilityFormal Aspects of Computing, 1994
- Reliable computation by formulas in the presence of noiseIEEE Transactions on Information Theory, 1988