ASTRAIL

News

Product line models of large cyber-physical systems: the case of ERTMS/ETCS

to be submitted to the Systems and Software Product Line Conference (SPLC), Gothenburg, Sweden, September 2018.

The paper applies a product line approach to the family of ERTMS/ETCS train control systems and to some of their foreseen extensions, as studied in the context of Shift2Rail and ASTRail.

Ten Diverse Formal Models for a CBTC Automatic Train Supervision System

See the link

by Franco Mazzanti and Alessio Ferrari (ISTI).

The paper has been presented at the 3rd Workshop on Models for Formal Analysis of Real Systems, Thessaloniki, Greece. Electronic Proceedings in Theoretical Computer Science Issue 268. Describes the encoding a train dispatching problem in the context of a CBTC system using ten different verification frameworks comparing the analogies and differences of the various approaches.

On the Industrial Uptake of Formal Methods in the Railway Domain: A Survey with Stakeholders

by Davide Basile, Maurice H. ter Beek, Alessandro Fantechi Stefania Gnesi, Franco Mazzanti, Andrea Piattino, Daniele Trentini, and Alessio Ferrari. The paper will be presented at the iFM conference on Formal Methods, Dublin, Ireland, September 2018. To appear in the Lecture Notes in Computer Science series, Springer.

Describes the results of the questionnaire on formal methods applications to railway systems, and it is one of the output of WP4.

Performance Analysis of FLL Schemes to Track Swept Jammers in an Adaptive Notch Filter

by Micaela Troglia Gamba and Emanuela Falletti, Istituto Superiore Mario Boella, Italy. Paper submitted to the NAVITEC 2018 conference, ESA-ESTEC, The Netherlands, December 5-7, 2018.

The paper is focused on the activity performed in the framework of WP 1, T1.6-GNSS Algorithm Analysis and Design of ASTRail. In particular, it faces the issue of GNSS Radio Frequency Interference (RFI), proposing a detection and mitigation method.

Towards Formal Methods Diversity in Railways: an Experience Report with Seven Frameworks

See the link

by Franco Mazzanti, Alessio Ferrari and Giorgio O. Spagnolo (ISTI-CNR). Software Tools for Technology Transfer Vol 20 (2018) (http://rdcu.be/ID78 ).

The paper exemplifies the issue of formal methods diversity by applying seven different verification frameworks for the verification of a train scheduling problem.

An HW-In-the-Loop Approach for the Assessment of GNSS Local Channel Effects in the Railway Environment

by Gianluca Falco, Mario Nicola, and Emanuela Falletti, Istituto Superiore Mario Boella, Italy. Paper to be published at ION GNSS+ 2018 conference, Miami (Florida), September 24-28, 2018

The paper describes the insertion of state-of-the-art channel model, named Land Mobile Satellite Channel Model (LMSCM), into a hardware-in-the-loop system, where the parameters generated by LMSCM are used to configure an RF GNSS signal generator. The use of the hardware generator eases the simulation of the entire GNSS constellation and the availability of the RF signal enables the assessment of the effects of rail-domain multipath on commercial receivers. The resulting model, named Rail-Land Mobile Satellite Channel Model (Rail-LMSCM), has been enhanced with the support of different kind of scenarios a train may encounter around the rail track, as well as the introduction of GNSS outages due to the presence of tunnels. Such enhancements make the Rail-LMSCM a more realistic average representation of the railway environment.

Formal Methods for the Railway Sector

See the link

by Maurice ter Beek, Alessandro Fantechi, Alessio Ferrari, Stefania Gnesi (ISTI-CNR, Italy), and Riccardo Scopigno (ISMB, Italy). Published in the ERCIM NEWS, January 2018.

Researchers from the Formal Methods and Tools group of ISTI-CNR are working on a review and assessment of the main formal modelling and verification languages and tools used in the railway domain, with the aim of evaluating the actual applicability of the most promising ones to a moving block signaling system model provided by an industrial partner. The research is being conducted in the context of the H2020 Shift2Rail project ASTRail.

Survey on Formal and Semi-formal Methods in Railways

See the link

Within ASTRail WP4, we have designed a short survey oriented to practitioners and academics with an interest in the application of formal and semi-formal methods to the development of railway systems.

Our goal is to understand what is the experience of the respondents in the application of formal and semi-formal methods in railways, and what are the main requirements that formal and semi-formal tools should have to be applied in the railway industry.

Please take our 5 minutes survey at the following link: https://goo.gl/forms/26wqR8Qt3vfxNfRv1