A refinement-based development of a distributed signalling system

The decentralised railway signalling systems have a potential to increase capacity, availability and reduce maintenance costs of railway networks. However, given the safety-critical nature of railway signalling and the complexity of novel distributed signalling solutions, their safety should be guar...

Full description

Saved in:
Bibliographic Details
Published in:Formal aspects of computing 2021-12, Vol.33 (6), p.1009-1036
Main Authors: Stankaitis, Paulius, Iliasov, Alexei, Kobayashi, Tsutomu, Aït-Ameur, Yamine, Ishikawa, Fuyuki, Romanovsky, Alexander
Format: Article
Language:English
Subjects:
Complex systems
Complexity
Computer Science
Formal method
Maintenance costs
Math Applications in Computer Science
Methodology
Modelling
Original Article
Rail transportation
Railroad signaling equipment
Railway networks
Railways
Safety critical
Signalling systems
Theory of Computation
Transportation networks
Verification
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The decentralised railway signalling systems have a potential to increase capacity, availability and reduce maintenance costs of railway networks. However, given the safety-critical nature of railway signalling and the complexity of novel distributed signalling solutions, their safety should be guaranteed by using thorough system validation methods. To achieve such a high-level of safety assurance of these complex signalling systems, scenario-based testing methods are far from being sufficient despite that they are still widely used in the industry. Formal verification is an alternative approach which provides a rigorous approach to verifying complex systems and has been successfully used in the railway domain. Despite the successes, little work has been done in applying formal methods for distributed railway systems. In our research we are working towards a multifaceted formal development methodology of complex railway signalling systems. The methodology is based on the Event-B modelling language which provides an expressive modelling language, a stepwise development and a proof-based model verification. In this paper, we present the application of the methodology for the development and verification of a distributed protocol for reservation of railway sections. The main challenge of this work is developing a distributed protocol which ensures safety and liveness of the distributed railway system when message delays are allowed in the model.
ISSN:0934-5043
1433-299X
DOI:10.1007/s00165-021-00567-y