title: Better maintenance of trains via model checking
company: NS
keywords: Maintenance, data, fault trees
topics: Case studies and Applications
committee: Carlos Esteban Budde ,
Mariëlle Stoelinga


Context. NedTrain is a subsidary of the Dutch Railroads (Nederlandse Spoorwegen) which is responsible for the maintenance of rolling stock (trains, locomotive, railroad cars etc). To improve their maintance strategy, NedTrain likes get more insight the reliability, failure modes, maintenance rules etc.

The research problem. Recently, NedTrain has introduced fault trees extended with maintenance as a modeling formalism, and used model checking to evaluate these fault trees. This worked pretty well, but there were two issues that we not solved yet:

1. The modeling of maintenance plans was quite ad hoc in the model checker, rather than as a systematic method in the fault tree. So, goal is to provide a more generic language to describe maintenance plans.

2. Earlier, we analyzed a single component. It would however be desirable model to the entire stock (ie all components in use and spare components in warehouses).

The MSc assignment. Thus, the goal of this assignment is to do a real-life case study at NedTrain and solve at least one of the mentioned issues.


1. Get acquinted with Fault Trees and maintenance

2. Model a real-life case study

3. Evaluate the performance with model checking



During Corona times, NS is facing problems, so we need to see what can be done


  1. Website NedTrain (Digital version available here)