Toward Formal Safety and Performance Evaluation of GNSS-based Railway Localisation Function

摘要

European Train Control System (ETCS) is the signalling and control component of the European Rail Traffic Management System (ERTMS). This system is essential to guarantee the safe and interoperable operation of trains. To enhance the competitiveness of rail transport services, the introduction of innovative solutions are under study in view of the evolution of ETCS. In this context, the adoption of Global Navigation Satellite System (GNSS) for train localization is investigated as a technology which can ensure an undeniable added value for railways. Yet, a main challenge is to provide safety evidence permitting the certification of these new systems. In particular, the classical safety analysis approaches show limitations in dealing with the complexity of such systems. Therefore, more adapted safety and performance analysis techniques have to be elaborated. In this paper, a model-based approach, adapted for the evaluation of GNSS-based localisation systems in railway, is presented. Considering the safety-critical aspect of the localisation function in railways, formal methods which are based on rigorous mathematical foundations are adopted in the present work. Concretely, a set of formal models are elaborated to ensure a modular representation of trains dynamics in the context of GNSS-based localization. Namely, probabilistic timed automata formalisms are adopted to this aim. Such notations allow for considering stochastic and dynamic aspects, so as to reflect reality in a trustworthy way. The safety and performance properties to be checked can then be formulated by means of temporal logics. Finally, the analysis of such features can be achieved by means of model-checking and simulation techniques. This evaluation phase yields both qualitative and quantitative results and allows for assessing the impact of various parameters and functional choices on both safety and performance. UPPAAL-SMC engine was used to set the tooling chain of our approach, and an illustration considering specific operational test cases is provided.