A refinement-based development of a distributed signalling system

Autor: Alexander Romanovsky, Fuyuki Ishikawa, Paulius Stankaitis, Alexei Iliasov, Yamine Ait-Ameur, Tsutomu Kobayashi
Rok vydání: 2021
Předmět:
Zdroj: Formal Aspects of Computing. 33:1009-1036
ISSN: 1433-299X
0934-5043
DOI: 10.1007/s00165-021-00567-y
Popis: 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.
Databáze: OpenAIRE
Externí odkaz: