Abstract In this paper we describe an industrial experience in the verification of the logic of a Railway Protection System (RPS). The RPS is designed within AIDA, a structured model-based design workflow and toolset. The RPS is written in a domain specific language amenable to signaling engineers, that is converted into Extended Finite State Machines (EFSM), and then into executable code. The RPS is parameterized, i.e., it can be applied, after configuration, in different operational scenarios. The logic is divided in classes, that are instantiated depending on the specific application. The verification challenge is to ensure that the required properties hold for all possible instantiations . We follow a verification approach based on the use of deductive methods, leveraging the Dafny framework. The AIDA environment is used to translate the RPS logic into Dafny, and also to automatically generate the contracts summarizing the methods implementing the guards and effects of the EFSM transitions. This approach greatly limits the need for human interaction with the underlying Dafny proof engine. In addition to domain specific optimizations, it results in an automated and efficient proof of the RPS properties.

Abstract We work in the context of a tool set developed for the Italian Railway Network supporting the migration of legacy relay-based interlocking systems to a new software-based implementation. We propose to generate test cases from the analog implementation in a way that they are significant for a comparison with a cycle-based computational model, by leveraging stable states abstraction. Our methodology found actual bugs in the new code that were missed by other analyses, and aids in documenting the expected differences with the legacy behaviors.

The railway domain is regulated by rigorous safety standards to ensure that specific safety goals are met. Often, safety-critical systems rely on custom hardware-software components that are built from scratch to achieve specific functional and non-functional requirements. Instead, the (partial) usage of Commercial Off-The-Shelf (COTS) components is very attractive as it potentially allows reducing cost and time to market. Unfortunately, COTS components do not individually offer enough guarantees in terms of safety and security to be used in critical systems as they are. In such a context, RFI (Rete Ferroviaria Italiana), a major player in Europe for railway infrastructure management, aims at equipping track-side workers with COTS devices to remotely and safely interact with the existing interlocking system, drastically improving the performance of maintenance operations. This paper describes the first effort to update existing (embedded) railway systems to a more recent cyber-physical system paradigm. Our Remote Worker Dashboard (RWD) pairs the existing safe interlocking machinery alongside COTS mobile components, making cyber and physical components cooperate to provide the user with responsive, safe, and secure service. Specifically, the RWD is a SIL4 cyber-physical system to support maintenance of actuators and railways in which COTS mobile devices are safely used by track-side workers. The concept, development, implementation, verification, and validation activities to build the RWD were carried out in compliance with the applicable CENELEC standards required by certification bodies to declare compliance with specific guidelines.

In this paper, a software-based resolver to digital converter (RDC) is proposed. The hardware signal conditioning circuit is realized using common electronic components, while the algorithm can be implemented either using a microcontroller or an FPGA. Its validation and performance analysis has been carried out using an interior permanent magnet synchronous machine drive and, with comparative purposes, an LTN Servotechnik 1024 ppr incremental encoder. Tests show that the proposed RDC is characterized by a good dynamic response and precision, moreover, due to low computational demand, it can be successfully adopted without significant extra cost.

Abstract We present Norma, a tool for the modeling and analysis of Relay-based Railways Interlocking Systems (RRIS). Norma is the result of a research project funded by the Italian Railway Network, to support the reverse engineering and migration to computer-based technology of legacy RRIS. The frontend fully supports the graphical modeling of Italian RRIS, with a palette of over two hundred basic components, stubs to abstract RRIS subcircuits, and requirements in terms of formal properties. The internal component based representation is translated into highly optimized Timed nuXmv models, and supports various syntactic and semantic checks based on formal verification, simulation and test case generation. Norma is experimentally evaluated, demonstrating the practical support for the modelers, and the effectiveness of the underlying optimizations.

Cascaded H-Bridges Multilevel Inverters are an innovative and promising solution in different application fields. This topology allows obtaining an improvement in the performance (e.g. reduced harmonic content, the low voltage stress on power components, and high efficiency) in respect to the traditional two-level inverters. In this context, the Multicarrier-PWM strategies play an important role thanks to their features. This paper presents an experimental investigation on the performance of a three-phase five-level Cascaded H-Bridge inverter by using different PWM modulation strategies. In particular, the paper is focused on the experimental validation of the main features of Multicarrier PWM taken into account by varying the modulation index and the switching frequency.

The ability to detect, localize and classify objects that are anomalies is a challenging task in the computer vision community. In this paper, we tackle these tasks developing a framework to automatically inspect the railway during the night. Specifically, it is able to predict the presence, the image coordinates and the class of obstacles. To deal with the low-light environment, the framework is based on thermal images and consists of three different modules that address the problem of detecting anomalies, predicting their image coordinates and classifying them. Moreover, due to the absolute lack of publicly-released datasets collected in the railway context for anomaly detection, we introduce a new multi-modal dataset, acquired from a rail drone, used to evaluate the proposed framework. Experimental results confirm the accuracy of the framework and its suitability, in terms of computational load, performance, and inference time, to be implemented on a self-powered inspection system.

Relay Interlocking Systems (RIS) are analog electromechanical networks traditionally applied in the safety-critical domain of railway signaling. RIS consist of networks of interconnected components such as power supplies, contacts, resistances, and electrically-controlled contacts (i.e. the relays). Due to cost and flexibility needs, RIS are progressively being replaced by equivalent computer-based systems. Unfortunately, RIS are often legacy systems, hard to understand at an abstract level, hence the valuable information they encoded in them is not available.In this paper, we propose a methodology and a tool chain to analyze and understand legacy RIS. A RIS is reduced to a Switched Multi-Domain Kirchhoff Network (SMDKN), which is in turn compiled into hybrid automata. SMT-based model checking supports various forms of formal analyses for SMDKN. The approach is based on the modeling of the RIS analog signals (i.e. currents and voltages) over continuous time, and their mapping in terms of railways control actions. Starting from the diagram representation, we overcome a key limitation of previous approaches based on purely Boolean models, i.e. the presence of spurious behaviors. The evaluation of the tool chain on a set of industrial-size railway RIS demonstrates practical scalability.