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)
![]()
|
Text
RW_Verification_Surrey_Tech_Report.pdf Available under License : See the attached licence file. Download (592kB) |
|
![]()
|
Text (licence)
SRI_deposit_agreement.pdf Download (33kB) |
Abstract
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 : |
|
||||||||||||||||||
Date : | 2012 | ||||||||||||||||||
Depositing User : | Symplectic Elements | ||||||||||||||||||
Date Deposited : | 29 Jun 2012 12:39 | ||||||||||||||||||
Last Modified : | 31 Oct 2017 14:39 | ||||||||||||||||||
URI: | http://epubs.surrey.ac.uk/id/eprint/711613 |
Actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year