Smart railroad maintenance engineering with stochastic model checking, in

RAMS (Reliability, Availability, Maintenance, Safety) requirements are utmost im-portant for safety-critical systems like railroad infrastructure and signaling systems, and often imposed by law or other government regulations. Fault tree analysis (FTA, for short) is a widely applied industry standard for RAMS analysis [1, 2], and is of-ten one of the techniques preferred by railways organizations [3]. FTA yields sys-tem availability and reliability, and can be used for critical path analysis. It can however not yet deal with a pressing aspect of railroad engineering: maintenance. While railroad infrastructure providers are focusing more and more on managing cost/performance ratios, RAMS can be considered as the performance specification, and maintenance the main cost driver. Methods facilitating the management of this ratio are still very uncommon. This paper presents a powerful, flexible and transparent technique to incorporate a maintenance aspects in fault tree analysis, based on stochastic model checking. We are able to analyze and compare different maintenance strategies (such as age-based, clock-based and condition-dependent maintenance) and their impact on reliability and availability metrics. Thus, we facilitate the trade off between cost and RAMS perfor-mance. To keep the underlying state space of our state space small, we deploy two aggres-sive state space reduction techniques, namely compositional aggregation, and smart semantics. We illustrate our approach on several existing, large fault tree models in a case study from Movares, a major RAMS consultancy firm in the Netherlands