Towards a Model-Based Safety Assessment of Railway Operation Using GNSS Localization

The introduction of satellite-based localization techniques, relying on GNSS (Global Navigation Satellite Systems), for railway operation is a promising, though challenging issue. Such a technical breakthrough aims to achieve a substantial gain for the railway sector in terms of competitiveness. In recent years, several projects have investigated the introduction of GNSS in railways. However, no proposed solution has been proven to fulfill the railway safety requirements. Moreover, traditional safety assessment methods present limitations in dealing with the complexity of such systems, raising the need to set up new approaches to this aim. The work discussed in this paper is part of a general model-driven approach for safety evaluation of GNSS-based localization in railway operation. In particular, we discuss the main features of our model-based approach and we elaborate on the different safety features that can be investigated based on our models. Considering the safety-critical aspect of the localization function, formal verification methods based on model-checking are adopted to provide safety evidence. Concretely, the overall behavior of the system will be expressed in a modular representation based on the timed automata notation supported by the UPPAAL tool. Such a modular approach permits to consider a variety of system architectures in different operational contexts. We also provide an illustration while taking into account a particular viewpoint that focuses on the operational context. This work can be seen as a first attempt towards adopting model-driven techniques for assessing and qualifying GNSS-based localization systems for railway operation.