Report on the results achieved by the project in the application of the proposed modeling and evaluation methods to the considered 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 for energy savings and taking into account failures, criticalities, and priorities of the system under analysis. The developed solutions have been 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. This deliverable reports the results of the application of the techniques that have been identified in the previous work [1] to the case studies. Specifically, Chapter 2 discusses the application of compositional methods for interlocking verification and the application of interfaces for testing the adequacy of the abstraction level; Chapter 3 addresses the application of methods for the quantitative evaluation of dependability to railway case studies; and Chapter 4 illustrates the application of methods for the quantitative evaluation of trade-offs between dependability properties and energy consumption to railway switch heater anti-icing systems.