University of Surrey

Test tubes in the lab Research in the ATI Dance Research

On modelling and verifying railway interlockings: Tracking train lengths

James, P, Moller, F, Nga Nguyen, H, Roggenbach, M, Schneider, S and Treharne, H (2014) On modelling and verifying railway interlockings: Tracking train lengths Science of Computer Programming, 96 (P3). pp. 315-336.

[img]
Preview
Text
SCPpaper.pdf - ["content_typename_Accepted version (post-print)" not defined]
Available under License : See the attached licence file.

Download (444kB) | Preview
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf
Available under License : See the attached licence file.

Download (33kB) | Preview

Abstract

The safety analysis of interlocking railway systems involves verifying freedom from collision, derailment and run-through (that is, trains rolling over wrongly-set points). Typically, various unrealistic assumptions are made when modelling trains within networks in order to facilitate their analyses. In particular, trains are invariably assumed to be shorter than track segments; and generally only a very few trains are allowed to be introduced into the network under consideration. In this paper we propose modelling methodologies which elegantly dismiss these assumptions. We first provide a framework for modelling arbitrarily many trains of arbitrary length in a network; and then we demonstrate that it is enough with our modelling approach to consider only two trains when verifying safety conditions. That is, if a safety violation appears in the original model with any number of trains of any and varying lengths, then a violation will be exposed in the simpler model with only two trains. Importantly, our modelling framework has been developed alongside - and in conjunction with - railway engineers. It is vital that they can validate the models and verification conditions, and - in the case of design errors - obtain comprehensible feedback. We demonstrate our modelling and abstraction techniques on two simple interlocking systems proposed by our industrial partner. As our formalization is, by design, near to their way of thinking, they are comfortable with it and trust it.

Item Type: Article
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
James, PUNSPECIFIEDUNSPECIFIED
Moller, FUNSPECIFIEDUNSPECIFIED
Nga Nguyen, HUNSPECIFIEDUNSPECIFIED
Roggenbach, MUNSPECIFIEDUNSPECIFIED
Schneider, SUNSPECIFIEDUNSPECIFIED
Treharne, HUNSPECIFIEDUNSPECIFIED
Date : 15 December 2014
Identification Number : 10.1016/j.scico.2014.04.005
Additional Information : NOTICE: this is the author’s version of a work that was accepted for publication in Science of Computer Programming. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in Science of Computer Programming, 96(P3), December 2014, DOI 10.1016/j.scico.2014.04.005.
Depositing User : Symplectic Elements
Date Deposited : 28 Jan 2015 10:37
Last Modified : 28 Jan 2015 10:37
URI: http://epubs.surrey.ac.uk/id/eprint/807107

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800