University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Combining event-based and state-based modelling for railway verification

Moler, F, Nguyen, HN, Roggenbach, M, Schneider, SA and Treharne, H (2012) Combining event-based and state-based modelling for railway verification Technical Report. (Unpublished)

Available under License : See the attached licence file.

Download (592kB)
Text (licence)

Download (33kB)


This paper is concerned with the formal modelling of sig- nalling and point control in the domain of railway engineering. Rules for handling interlocking to ensure railway safety and liveness are often intricate and challenging to verify. We develop a CSP||B model taking a “natural modelling” approach, where the models are as close as possible to the domain model, providing traceability and ease of understanding to the domain expert. This leads to a natural separation between the global modelling of the tracks in B, and the CSP encapsulation of the local views of the individual trains following the driving rules. The ap- proach is illustrated through a small case study (Mini-Alvey), and the model provides verification through formal proofs or informative counter example traces if verification fails.

Item Type: Monograph (Technical Report)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
Moler, F
Nguyen, HN
Roggenbach, M
Schneider, SA
Treharne, H
Date : 2012
Depositing User : Symplectic Elements
Date Deposited : 29 Jun 2012 12:39
Last Modified : 31 Oct 2017 14:39

Actions (login required)

View Item View Item


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