On Modelling and Verifying Railway Interlockings: Tracking Train Lengths
Tools
Tools
Tools
James, P, Moller, F, Nguyen, HN, Roggenbach, M, Schneider, SA and Treharne, H (2013) On Modelling and Verifying Railway Interlockings: Tracking Train Lengths Technical Report.
![[img]](http://epubs.surrey.ac.uk/style/images/fileicons/text.png)
|
Text
TechReport-CS-13-03.pdf Available under License : See the attached licence file. Download (702kB) |
|
|
Text (licence)
SRI_deposit_agreement.pdf Download (33kB) |
Official URL: http://www.surrey.ac.uk/computing/index.htm
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 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: | Monograph (Technical Report) | |||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Divisions : | Faculty of Engineering and Physical Sciences > Computing Science | |||||||||||||||||||||
| Authors : |
|
|||||||||||||||||||||
| Date : | 19 May 2013 | |||||||||||||||||||||
| Uncontrolled Keywords : | Railway verification, CSP||B, modelling and analysis. | |||||||||||||||||||||
| Related URLs : | ||||||||||||||||||||||
| Depositing User : | Symplectic Elements | |||||||||||||||||||||
| Date Deposited : | 10 Jul 2013 15:23 | |||||||||||||||||||||
| Last Modified : | 31 Oct 2017 15:05 | |||||||||||||||||||||
| URI: | http://epubs.surrey.ac.uk/id/eprint/775069 |
Actions (login required)
 |
View Item |
Downloads
Downloads per month over past year