Output details
11 - Computer Science and Informatics
University of Surrey
Defining and Model Checking Abstractions of Complex Railway Models Using CSP||B
<11>This paper provides a new formal abstraction, applicable to general modelling of railway scheme plans, to improve the feasibility of model checking railway signalling interlocking systems that traditionally suffer from state space explosion. Invensys (now Siemens) considers it one of the most promising ways of analysing their interlocking systems. It is significant within the new UK Rail Technical Strategy, which has “ensuring safety and enhancing capacity” as a central theme, as control systems are being rearchitected over the next decade to fit with new European standards. Formal analysis techniques are now essential given the complexity of next generation control systems.