
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.
Share this article

Learn to build a solid safety case for rail control systems using formal verification
Fill out your information here.
More News & Articles
Prover is partnering with Eiffage Énergie Systèmes on the Villeneuve Demain project, delivering railway signaling software for the PAVS system at SIL4 safety level.
Using Prover’s automation tools, the solution ensures EN 50716 compliance, facilitates future maintenance, and enables reuse across similar systems.
Prover will be at Train & Rail, meet us in our booth located at A06:31.
Learn how Prover’s Relay Signaling Migration enables safe, efficient modernization of legacy railway systems with formal verification and digital twin technology.