A Markov Reward Model for Software Reliability

A compositional method for estimating software reliability of many threaded programs is developed. The method uses estimates of the reliability of individual modules and the probability of transitions between the modules to estimate the reliability of a program in terms of its current state. The reliability of a program is expressed using iLTL, a probabilistic linear temporal logic whose atomic propositions are linear inequalities about transitions of the probability mass function of a discrete time Markov chain. We then use a Markov reward model to estimate software reliability. The technique is illustrated in terms of an example.