Formal methods and standard interfaces will be the topic of a work package within the European Shift2Rail (S2R) Joint Undertaking, which includes all major European signalling system suppliers and a number of infrastructure managers. This work package is led by the Swedish Transport Administration (Trafikverket), who is a founding member of Shift2Rail. Prover is proud to have been selected to assist Trafikverket in this work, acting as deputy manager for this work package.
Formal Verification will reduce complexity
Over the last 10 years or so, formal methods have matured, and in particular, formal verification has matured considerably, with examples of mature use in safety assessment of rail control software. Formal verification will be a key topic in this work package, due to its potential to significantly reduce the complexity, effort and cost of safety assessment of rail control software. While standard interfaces constitute an orthogonal aspect to formal methods (one can use one without the other), they can be a key driver to increase competition, and enable more efficient application (and reuse) of formal methods, in order to reach the objectives of this work package:
• Save cost in signalling system life-cycle (LCC)
• Support independent lifetime of sub-systems in the control command and signalling system
• Increase market competition and standardisation
• Improve interoperability and reliability
• Shorten time-to-market of new products
• Increase know-how of formal methods in railway signalling
This work package is scheduled to start in the fall of 2017. Around this time, interface specifications shall be published by EULYNX, which is an initiative focusing on the development of standardized interfaces between interlocking and adjacent systems. These specifications will be interesting to evaluate for possible inclusion into this work package. For more information, stay tuned later on in 2017.
If you do not follow our blog you can fill out the form to the right.
Share this article
Learn more about how to develop specifications with Digital Twins
Fill out your information here.
More News & Articles
Prover introducing Signaling Design Automation to students at CentraleSupélec in Paris
Prover PSL, the leading model checker used for formal verification in the rail and metro signaling domain, is now even faster.
Prover and RATP Strengthen Collaboration: Advancing Passenger Safety with Formal Methods.