[NPKS05] Gethin Norman, David Parker, Marta Kwiatkowska and Sandeep Shukla. Evaluating the Reliability of NAND Multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(10), pages 1629-1637. October 2005. [ps.gz] [pdf] [bib] [Analyses the reliability of defect-tolerant design, NAND multiplexing, using PRISM.]
Downloads:  ps.gz ps.gz (82 KB)  pdf pdf (218 KB)  bib bib
Notes: Further information and verification results are available from the case study web page.
Abstract. Probabilistic model checking is a formal verification technique for analysing the reliability and performance of systems exhibiting stochastic behaviour. 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 behaviour of the system. This allows a designer to evaluate, for example, the trade-off between redundancy and reliability in the design. We also highlight errors in analytically computed reliability bounds, recently published for the same case study.