Better maintenance of trains with model checking

title:Better maintenance of trains with model checking
contact:dr. M.I.A. Stoelinga
to be started:any time


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.

Recently, NedTrain has introduced fault trees extended with maintenance as a modeling formalism, and used model checking to evaluate these fault trees. The goal of this internship is to further apply fault tree analysis and model checking in the NedTrain context.

Typical topics to work on are:

- modeling of maintenance strategies. Currently, maintenance rules (eg daily inspections, preventive replacements, etc) are encoded in the model checker. We would like to have a language to specify these rules in the faul tree.

- larger case studies: in earlier work, we modeled one train compressor. However, NedTrain has 180 compressors in its trains, and 60 spare compressors. Can we compute the reliability of the entire stock from the reliability of

- reliability specifications & computations: if we set a reliability requirement (say: reliability = 1 - 10^-9) can we then automatically compute the reliability for the components?

- Other relevant topics are possible as well.



  1. webpage nedtrain (Digital version available here)