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 |
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
This Page was prepared by Mark Jorgensen.