Techniques for modelling and verifying railway interlockings
- Submitting institution
-
Swansea University / Prifysgol Abertawe
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 21770
- Type
- D - Journal article
- DOI
-
10.1007/s10009-014-0304-7
- Title of journal
- International Journal on Software Tools for Technology Transfer
- Article number
- -
- First page
- 685
- Volume
- 16
- Issue
- 6
- ISSN
- 1433-2779
- Open access status
- Out of scope for open access requirements
- Month of publication
- March
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
-
- Research group(s)
-
-
- Citation count
- 14
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Verification of railway interlockings, the basis of signalling, has been a long-standing challenge for Computer Science due to scalability. Here is the first proven correct general decomposition technique for verifying interlockings. This technique decomposes railway scheme plans into a set of smaller plans for verification, solving the scalability problems notorious in the field. We demonstrate the applicability of the approach to real world interlockings and provide the foundations for broader use. Rail research groups all over the world have now incorporated decomposition within their verification frameworks. The work underpins the Railway Verification impact case study submitted by Swansea Computer Science.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -