Browse by author
Lookup NU author(s): Dr Sergiy BogomolovORCiD, Dr Alexei Iliasov, Emeritus Professor Alexander RomanovskyORCiD, Dr Paulius Stankaitis
This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).
Over the last few decades, the safety assurance of cyber-physical systems has become one of the biggest challenges in the field of model-based system engineering. The challenge arises from an immense complexity of cyber-physical systems which have deeply intertwined physical, software and network system aspects.With significant improvements in a wireless communication and microprocessor technologies, the railway domain has become one of the frontiers for deploying cyber-physical signalling systems. However, because of the safety-critical nature of railway signalling systems, the highest level of safety assurance is essential. For years formal methods have been successfully applied in the railway domain to formally demonstrate safety of railway systems. Despite that little has been done in the field of formal methods to address the cyber-physical nature of modern railway signalling systems. In this paper we present an approach for a formal development of cyber-physical railway signalling systems which is based on a refinement driven modelling and proof-based verification. Our approach utilises the Event-B formal specification language together with a hybrid system and communication modelling patterns to developing a generic hybrid railway signalling system model which can be further refined to capture a specific railway signalling system.
Author(s): Ait-Ameur Y, Bogomolov S, Dupont G, Iliasov A, Romanovsky A, Stankaitis P
Publication type: Article
Publication status: Published
Journal: Formal Aspects of Computing
Year: 2023
Volume: 35
Issue: 1
Print publication date: 12/01/2023
Online publication date: 27/08/2022
Acceptance date: 02/03/2022
Date deposited: 07/06/2022
ISSN (print): 0934-5043
ISSN (electronic): 1433-299X
Publisher: ACM
URL: https://doi.org/10.1145/3524052
DOI: 10.1145/3524052
ePrints DOI: 10.57711/j3nf-p915
Altmetrics provided by Altmetric
