Combining event-based and state-based modelling for railway verification
F Moler, Hoang Nga Nguyen, Markus Roggenbach, Steve A. Schneider, Helen Treharne · Surrey Research Insight Open Access (The University of Surrey) · 2012
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.