Final Report of the COST-247 Action

AN EXPERIMENT IN FORMALISING AND ANALYSING RAILYARD CONFIGURATIONS

Lars-ake Fredlund and Fredrik Orava

 KTH/Teleinformatik Electrum 204 S-164 40 KISTA SWEDEN Tel: +46 8 752 1490 Fax: +46 751 1793 E-mail: fredrik@it.kth.se , fred@sics.se

### 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.

This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).

COST-247 Working Group(s): 1-2