Optimal spare management via statistical model checking: a case study in research reactors

Abstract Systematic spare management is important to optimize the twin goals of high reliability and low costs. However, existing approaches to spare management do not incorporate a detailed analysis of the effect on the absence of spares on the system’s reliability. In this work, we combine fault tree analysis with statistical model checking to model spare part management as a stochastic priced timed game automaton (SPTGA). We use Uppaal Stratego to find the number of spares that minimizes the total costs due to downtime and spare purchasing. The resulting SPTGA model can then additionally be analyzed according to a wide range of other metrics, including expected availability. We apply these techniques to the emergency shutdown system of a research nuclear reactor. In this case study, the failure probability is low, so we change the settings of Uppaal Stratego setting to obtain reliable results about rare events. We consider both a single subsystem and the combination of two subsystems. In both situations, our methods find the optimal number of spares, minimizing cost while ensuring an expected availability of 99.96% and 99.93%, respectively.