Summary

In the Sustainable Mobility objective, great emphasis is placed on promoting railways as a means of transport capable of reducing environmental impact and energy consumption, for which it is crucial to increase attractiveness of railway services in terms of frequency and capillarity. To this end, railway systems must guarantee a set of expected Key Performance Indicators (KPIs)such as safety of the train movement, capacity (e.g., number of trains or passengers per time unit), energy efficiency, operating cost… Nowadays, and even more in the future, these KPIs are determined by the collective operation of a number of innovative subsystems that cooperate to the smooth working of railway systems, notably supporting monitoring, command, and control of physical railway equipment.

The many specific and complex interactions among these subsystems raise new challenges that endanger accurate and efficient evaluation of KPIs, as well as safe interoperability. On the one hand, addressing them requires overcoming the limitations of state-of-the-art hierarchical and compositional techniques for estimation of non-functional attributes of component-based systems, to properly fit railway needs. On the other hand, advancements on formal specification of behavioral interfaces among heterogeneous components are advocated to improve the reliability of the composition of railway sub-systems while reducing their cost.

To address these challenges, the ADVENTURE project develops innovative solutions for the evaluation of railway systems. Using Model-Driven Engineering (MDE) methods and multi-paradigm or multi-formalism approaches to help create bridges between different abstraction levels, the project focuses on the following objectives:

Qualitative evaluation of safety of complex distributed railway systems, by means of diverse techniques such as compositional model checking, synthesis of specifications given as behavioral interfaces, and tool support for relating specifications with implementations; Quantitative evaluation of dependability attributes in spite of failures, in particular considering communication failures, through quantitative modeling and evaluation of the timed failure logic of the system; Quantitative evaluation of trade-offs between energy efficiency and availability/performance, considering different smart policies of energy saving and taking into account failures, criticalities, and priorities of the system under analysis.

The developed solutions will be validated by their application to systems highly representative of the innovation trends in railways, notably including decentralized interlockings and smart deicing systems.

To address these objectives, ADVENTURE unites two research units with consolidated experience in model-based methods for qualitative and quantitative evaluation of complex systems and in their application to various fields of the railway domain.

Publications

2024

  • Basile, D. and ter Beek, M.H.; Advancing orchestration synthesis for contract automata Journal of Logical and Algebraic Methods in Programming p.100998. link

  • Basile, D., Modelling, Verifying and Testing the Contract Automata Runtime Environment with Uppaal In International Conference on Coordination Models and Languages (pp. 93-110). Cham: Springer Nature Switzerland. link

  • Cortés, D., Ortiz, J., Basile, D., Aranda, J., Perrouin, G. and Schobbens, P.Y. Time for Networks: Mutation Testing for Timed Automata Networks In Proceedings of the 2024 IEEE/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE) (pp. 44-54). link

  • Basile, D., ter Beek, M. H., Carnevali, L., Chiaradonna, S., Di Giandomenico, F., Fantechi, A. and Gori, G. An Integrated Perspective on the Evaluation of Complex Railway Systems
    In Proceedings of the 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Application Areas (ISoLA’24) (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 15223, Springer, Cham, 2024, pp. 190 - 207. link

  • Basile, D., ter Beek, M.H., Di Giandomenico, F., Carnevali, L. and Fantechi, A. Advanced Integrated Evaluation of Railway Systems ERCIM News - Special: Extended Reality 137 (2024), pp. 53–54. link

  • Limbrée, C., Haxthausen, A. E., Gori, G., Fantechi, A., Formal Verification of Railway Interlockings: a Compositional Approach Based on a Library of Pre-verified Components In Proceedings of the 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation: Application Areas (ISoLA’24) (T. Margaria and B. Steffen, eds.), Lecture Notes in Computer Science 15223, Springer, Cham, 2024, pp. 127 - 141. link