PRIN PNRR Adventure D1.1 - Report on the definition of the case studies

ADVENTURE (ADVancEd iNtegraTed evalUation of Railway systEms) aims at developing innovative solutions for the evaluation of complex 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: 1) 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; 2) 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; 3) 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 are going to be experimented and validated by their application to different case studies, that are considered as representative of the innovation trends in railways, namely decentralized interlocking systems, standard interfaces and smart deicing systems. A common trait of these case studies is that they can be considered as distributed Cyber-Physical Systems that ensure safe transit of trains along a station route. In all cases, the route is allocated if specific conditions are verified on a set of elements lying along the route, with also an eye to the energy consumption in case the involved equipment are characterized by energy-intensive operation. A failure of one of these elements generally means that the itinerary is unavailable: in this case, the availability and thus the overall transit capacity of the station decreases as well, with the possible occurrence of single points of failure blocking all operations. Modeling such a complex system for the purpose of quantitative assessment of availability suffers from the problem of state-space explosion. It is therefore desired to: (a)~identify a model-based compositional method for analyzing such a complex network by combining results of the analysis of its elements, with the aim to perform network analysis in linear time with respect to the number of elements; the approach will be tried on some topological instances of the two case studies; (b)~generalize the identified approach so that it can be automatically instantiated on different network topologies, both for ADVENTURE case studies and for networks defining other distributed systems that have similar characteristics or similar dependability requirements.