Formal verification of movement authorities in automatic train control systems
Formal verification of movement authorities in automatic train control systems
- Author(s): S. Ghosh ; P. Dasgupta ; C. Mandal ; A. Katiyar
- DOI: 10.1049/cp.2016.0511
For access to this article, please select a purchase option:
Buy conference paper PDF
Buy Knowledge Pack
IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.
International Conference on Railway Engineering (ICRE 2016) — Recommend this title to your library
Thank you
Your recommendation has been sent to your librarian.
- Author(s): S. Ghosh ; P. Dasgupta ; C. Mandal ; A. Katiyar Source: International Conference on Railway Engineering (ICRE 2016), 2016 page ()
- Conference: International Conference on Railway Engineering (ICRE 2016)
- DOI: 10.1049/cp.2016.0511
- ISBN: 978-1-78561-292-3
- Location: Brussels, Belgium
- Conference date: 12-13 May 2016
- Format: PDF
The safe functioning of a train control system is critically dependent on the validity of the movement authorities issued to a train by the track-side radio control blocks (RBC). In order to guarantee that the movement authorities are safe, the RBC needs to consult the interlocking logic. The RBC and the interlocking logic has to be configured with data specific to the yard of operation. This paper aims to validate the data using formal methods. Specifically we present an approach for proving that the trains maintain safe distance between them when they follow the movement authorities issued by the RBC in a yard. We use UPPAAL [13] for modelling the train control system system for a small yard including the continuous dynamics of trains. The UPPAAL model-checker is used to verify the safety of all train movements permitted by the model. We demonstrate that errors in the logic can be detected by the proposed method in feasible time. As opposed to previous approaches using theorem proving techniques, our method lends itself easily to automation, which is thereby more acceptable to railway engineers.
Inspec keywords: control engineering computing; traffic engineering computing; rail traffic control; theorem proving; formal verification
Subjects: Control engineering computing; Traffic engineering computing; Rail-traffic system control; Formal methods
Related content
content/conferences/10.1049/cp.2016.0511
pub_keyword,iet_inspecKeyword,pub_concept
6
6