Abstract:

We present a method by which the abstract behaviour of railyards can be specified, and analysed for safety. Our analysis is based on well established railway signalling concepts such as {\em train routes} and {\em flank protection} and attempts to verify safety properties which state that if the railyard is configured in a correct way, no unwanted situations such as train collisions or derailings will occur. We specify the railyards in process algebra and the safety properties in the modal $\mu$-calculus.