Prover is proud to announce our integral role in the latest railway signaling project for the Orléans tramway. In Consortium with Fortil Mobility, ETF, SES Signalisation, Prover have secured a turnkey project that will see the adaptation of the existing signaling system to create a new intersection with Avenue Emile Bernon. This endeavor not only marks a significant milestone for our cluster but also underscores the cutting-edge technology and expertise that Prover brings to the table.

Our advanced automation solutions are at the heart of this project, ensuring that every aspect of the signaling system maintains its safety, efficiency, and reliability. Here’s how our products are making a difference:

Comprehensive design and development

Prover’s state-of-the-art software solutions are being utilized to update and validate the automation systems required for this project. Our product Prover iLock ensures that every component of the signaling system meets their requirements. The Schneider PLC code for non-vital logic developed initially with Control Expert has been uploaded to Prover iLock to connect it to the railway layout. In addition, a model of relay vital logic was created from the relay schematics. The combination of these two components, complemented by wayside objects behaviors, provides a working Digital Twin of complete interlocking.

Seamless integration and validation

One of the key challenges in railway signaling projects is ensuring that all systems work seamlessly together. Prover iLock is designed to facilitate smooth integration and rigorous validation processes. With Prover’s expert staff, we performed comprehensive testing and validation, ensuring that the signaling system operated flawlessly from day one. This reduces risks and accelerates the project timeline, with the commissioning scheduled for this summer.

Collaborative success

This project is a perfect example of how collaborative efforts can lead to outstanding results. Prover is proud to work alongside Fortil Mobility, ETF (Vinci group), and SES Signalisation to bring this project to fruition. Each partner brings unique expertise and capabilities, creating a synergy that drives the project forward.

In the realm of railway software development, adherence to industrial standards is not just a matter of compliance; it’s a cornerstone of ensuring safety, reliability, and efficiency in railway operations. The latest milestone in this journey is the introduction of the CENELEC standard EN 50716:2023. This new standard represents a significant leap forward from its predecessors, EN 50128:2011 and EN 50657:2017, while maintaining a smooth transition from its predecessors and a closer alignment with the railway RAMS standards (EN 50126 and EN 50129).

At Prover, we’ve been deeply involved in the landscape of railway software standards, providing compliant tools and applications for years. Now, as we delve into the nuances of the standard, we’re thrilled to share our insights and discoveries with you.

One of the standout features of EN 50716 is the expanded endorsement of formal methods across all Safety Integrity Levels (SILs), a testament to the growing efficiency and effectiveness of these techniques for rail systems. Moreover, the concept of “tool diversity”, introduced in previous standards and further solidified in EN 50716, opens new avenues for trust delegation among T2 and T3 tools¹, enhancing the robustness and flexibility of software development processes. These evolutions align seamlessly with our longstanding commitment to formal methods and the principles (regarding tool diversity) that have guided Prover’s product design for many years.

But evolution doesn’t stop there. Annex C of EN 50716 introduces fresh perspectives on software development, including guidance on two lifecycle models (linear versus iterative), modeling techniques, and the integration of Artificial Intelligence and Machine Learning (AI/ML). While iterative lifecycle models offer flexibility, they also demand careful navigation to maintain safety and regulatory compliance—a balance we’re well-equipped to address at Prover.

As for AI/ML, while their potential is undeniable, challenges in verification and validation of ML components within the context of EN 50716 remain. However, at Prover, we’re already exploring how these technologies can synergize with formal methods to drive innovation and efficiency.

Another notable change we wish to highlight before concluding this blog post is the major improvements made to software management and organization (clause 5) in EN 50716. These improvements eliminate outdated terminology, enhance clarity, and improve readability, thereby facilitating users to navigate standards with greater ease and flexibility while maintaining the same level of rigor.

¹ Model checkers (such as Prover’s PSL) and testing-related utilities fall into the class of T2 tools, which is specifically designed for verifying code or data. In contrast, T3 tools are involved in the creation or transformation of code, commonly represented by code compilers and generators.

Read the complete guide on CENELEC standard EN 50716 here!

From more than two months down to less than two weeks, or six times faster. From almost two weeks down to just five hours, or sixty times faster! These are the kind of speed ups that we are now obtaining in PSL (Prover SL CE) by boosting our turbo-threads technology using AI-optimized proof tactics. Make sure you read our previous blog post back in September, we have been working hard and made very good progress since then. Thanks again to Vinnova, Sweden’s Innovation Agency, for partially funding this R&D project!

The current state of AI-powered PSL

We have a research branch of PSL that has been modified to enable AI-tuned tactics to guide the model-checker during proof search. These proof tactics are obtained by a specialized AI-guided fine-tuning procedure, and they are designed to speed up specific sets of properties. Obtaining one such tactic could, in some cases, keep our servers busy for more than a week. Yet, the obtained tactic can mean saving months of CPU time and faster delivery times for our customers. These proof tactics do not only speed up verification for the HLL model that is used for training, but also boost verification for subsequent versions of the same model. We can fine-tune a proof tactic today and benefit from it for years.

This technology could already be highly valuable to some users of PSL who have very high demands for performance. And you may be able to benefit from it relatively soon! Initially we plan to offer this as a service, that is, you send us an HLL model and we send you back a set of customized proof tactics. For the future we are considering integrating our AI-guided fine-tuner into a special front-end for PSL, so that training happens automatically every time you solve a property.

What is coming next

We are currently experimenting with the computation of features that can characterize and relate a set of safety properties, that is, their “DNA” equivalent. Using this “DNA” will allow us to automatically discover properties that would benefit from known proof tactics, and also compute new proof tactics faster. At the same time, we have also started to explore prediction models, based on deep learning, that could automatically suggest the best proof tactic for a previously unseen property. All this put together would mean that, one day, all PSL users could automatically benefit from these AI-powered speed ups.

Let’s keep working on the future of formal verification!

On August 31, 2017, the Swedish Transport Administration’s Director General, Lena Erixon, submitted to the Swedish Government the “Proposal for National Transport Planning Plan 2018-2029”. Erixon points out that the starting point for this plan has been to work with, and contribute to an efficient, modern and sustainable transport system. This plan represents a financial framework of more than SEK 100 billion more than the current plan, and amounts to SEK 622.5 billion. In addition to this, 90 billion from, for example, railway charges, co-financing and congestion taxes are also included. For the railroad, this plan means an increased effort, made possible by increased funds, on robust and reliable transport. The transition from analogue to digital is emphasized by the potential of digitization, such as the introduction of ERTMS, giving the railroad clear progress.

Transport System 2018-2029 means new railroad

Among the investments proposed for the Swedish railroad are lanes throughout Stockholm – Uppsala, the first stretch of Norrbotniabanan, the last stage on Västkustbanan and many others. The Swedish Transport Administration claims that an increase in maintenance costs will affect both freight and commuting positively, as the railways functionality can be restored with these funds.

Better repairs and track changes will deliver a more reliable rail system

The increased funds will thus mean a more reliable rail system with fewer disturbances.
The plan also contains proposals for the reintroduction of speeds previously reduced, including current lanes in metropolitan areas. In order to counteract similar speed cuts in the future, the Swedish Transport Administration also proposes measures to reduce this risk, especially by continuing with performing repairs and track changes. Lanes that do not fall within this group will be comprised of a focus on the possibility of continued traffic and the maintenance of today’s functionality.

Functionality for speed, accessibility and maintenance of rail safety is highlighted by the Swedish Transport Administration as important in ongoing and future investments and work.

Signaling systems will be modernized

In addition, the proposal contains a focus on digitizing signaling systems and modernizing the Swedish signaling systems. On certain Swedish railways, the systems are over 50 years old and therefore need to be replaced. The Swedish Transport Administration therefore argues that during this period these will be successful during the period will be replaced according to ERTMS. In order to facilitate this work, the Swedish Transport Agency also proposes to investigate whether co-financing of ERTMS onboard equipment with existing EU contributions is possible.

As part of Swedish Transport Administration´s national plan there will be a lot of focus on innovations and in order for the railway to be competitive in the future, both digitization and automation need to be strengthened, both in project and delivery phase as well as in operation. The way to do this is to think outside the box and not only support traditional development methods.

The Swedish Transport Administration seeks an infrastructure for the future, with innovative solutions for strengthening competitiveness and sustainable development – this is entirely in line with Prover’s ambitions and products.

If you want better understand how modern signaling solutions should be designed and developed you can study our White Paper “Interlocking Design Automation – The Process”.

A modern solution will also make it possible to cut cost and drive efficiency. You can find more information in our White Paper “How to Build the Business Case for an Investment in a New Process for Interlocking Design Automation”.