View article

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is …