ePrints

A refinement-based development of a distributed signalling system

Lookup NU author(s): Dr Paulius Stankaitis, Dr Alexei Iliasov, Emeritus Professor Alexander RomanovskyORCiD

Downloads

• Published version [.pdf]

Licence

This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).

Abstract

The decentralisation of railway signalling systems has the potential to increase railway network capacity, availability and reduce maintenance costs. 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. In this paper, we present a rigorous formal development and verification of a distributed protocol for reservation of railway sections, which we believe could deliver benefits of a decentralised signalling while ensuring safety and liveness properties. For the formal distributed protocol development and verification, we used the Event-B formal specification language, which allows to reduce modelling and verification efforts by providing a formal modelling approach based on refinement.

Publication metadata

Author(s): Stankaitis P, Iliasov A, Kobayashi T, Ait-Ameur Y, Ishikawa F, Romanovsky A

Publication type: Article

Publication status: Published

Journal: Formal Aspects of Computing

Year: 2021

Volume: 33

Issue: 6

Pages: 1009-1036

Online publication date: 24/11/2021

Acceptance date: 30/09/2021

Date deposited: 30/09/2021

ISSN (print): 0934-5043

ISSN (electronic): 1433-299X

Publisher: Springer Nature

URL: https://doi.org/10.1007/s00165-021-00567-y

DOI: 10.1007/s00165-021-00567-y

Altmetrics

Funding

Share