On November 14-16th, the RSSRail Conference was held in Pistoia, Italy. The conference brought together researchers, engineers and academics from the rail industry, who are interested in building critical advanced railway applications and systems. Our Chief Strategy officer, Arne Borälv, was there to represent Shift2Rail and Trafikverket.
In November I attended the RSSR2017 Conference on Reliability, Safety and Security of Railway Systems: Modeling, Analysis, Verification and Certification. I was there to represent Shift2Rail and Trafikverket, and gave a brief overview presentation of its work package on formal methods, as part of the presentation slot for Shift2Rail. The presentation went well, and questions from the audience indicate there is interest in the results that will come from this work package.
Out of the many different presentations at the conference, these caught my interest:
-
Safety Analysis of a CBTC System
A Rigorous Approach with System Level B Industry ClearSy presented a retroactive safety analysis of a CBTC system at RATP, as an overlay over existing interlocking systems. ClearSy’s approach was based on manual identification of safety hazards and manual derivation of safety requirements, with “confirmation” by formalization and proof using the B method.
-
Deductive Verification of Railway Operations
Eduard Kamburjan presented work on formalization of Deutsche Bahn’s operational rules for conventional signaling, with verification of safety properties. This seemed like a nice application of formal methods, with a modelling language built on top of Erlang.
-
Are Standards an Ambiguity-Free Reference for Product Validation?
Mario Fusani presented tool-assisted analysis to detect issues in natural language specifications, such as vagueness and under-specification. They reported results from analyzing the EN 50128 standard and an ERTMS product specification (with the analysis pin-pointing less issues in the latter).
Formal Methods Case Study: Hybrid ERTMS/ETCS Level 3
At the conference, I learnt about a “formal methods case study” for the 2018 ABZ conference. The case study is based on the principles for Hybrid ERTMS/ETCS Level 3, specified by the ERTMS Users Group (EUG). The idea of this case study is to offer a real-life case study from the railway domain. The Hybrid ERTMS/ETCS Level 3 makes it possible to increase capacity using fixed virtual blocks, as an alternative to moving block. More information about the case study and the EUG specification can be found here.