Empowering the Future of Indian Railways

India is undertaking one of the world’s largest railway modernization initiatives, with KAVACH — the nation’s indigenous Automatic Train Protection (ATP) system — at its core. Through this partnership, Prover and BHEPL will focus on automating data preparation and verification for KAVACH deployments, enabling suppliers to streamline engineering workflows, reduce manual errors and improve overall safety. 

Leveraging Prover iLock, BHEPL will customize and automate the generation of essential datasets such as RFID tag layouts, control tables, gradient plans and other key KAVACH project deliverables. These activities, traditionally performed manually over several weeks, can now be completed in a fraction of the time with higher accuracy and consistency. 

Extending Automation to Metros and Beyond

Our collaboration extends beyond KAVACH. Prover and BHEPL are actively working with metro operators, Indian Railways, and signaling suppliers to explore broader automation opportunities — ranging from interlocking design to CBTC (Communication-Based Train Control) software development. Together, we aim to accelerate the deployment of safe, efficient, and digitally–verified signaling systems across India. 

A Shared Commitment to Safety, Reliability, and Efficiency

“India’s railway modernization drive presents an incredible opportunity to showcase how automation and formal methods can enhance safety, reliability and cost efficiency,” says Gunnar Smith, Chief Product Officer at Prover. “BHEPL’s strong engineering expertise, combined with our globally proven automation tools, is a powerful combination for achieving these goals.” 

Sudhir Reddy, Director at BHEPL, adds: 
“By partnering with Prover, we aim to bring world-class automation and verification capabilities to Indian Railways and metro systems. This collaboration aligns perfectly with India’s vision for a digitally transformed rail ecosystem. The automation tools and products we are co-developing with Prover will be a significant technological advancement for Indian Railways.” 

Introducing Prover iLock for KAVACH: Generative-AI–Driven Design Document Automation for Indian Railways

Prover and BHEPL are launching a Generative AI-powered solution, based on Prover iLock, designed specifically for automating signaling and KAVACH engineering documentation. 

This solution, co-engineered with BHEPL, uses Generative AI, formal methods and rule-based validation to: 

• Generate, verify and standardize complex signaling documents 

• Interpret datasets such as SIPs, TOCs, gradient plans and RFID tag layouts 

• Produce RDSO-compliant outputs automatically 

• Reduce engineering cycle times from weeks to hours 

With adaptive learning models tailored to Indian Railways, Prover iLock understands and evolves with: 

• National railway standards 

• KAVACH-specific data structures 

• Interlocking principles 

• RFID-based control logic 

This enables Prover iLock to function not only as a documentation tool but also as a simulation, verification and validation environment capable of: 

• Virtual testing of KAVACH configurations 

• Simulating interlocking behavior 

• Verifying tag placement logic 

• Ensuring fail-safe operation before field implementation 

These capabilities significantly reduce on-site testing time and accelerate certification. 

Upcoming CBTC Automation Module

Prover and BHEPL are finalizing a CBTC design automation module, marking a major advancement for India’s metro signaling ecosystem. By integrating Prover’s proven formal verification technologies, the CBTC extension will automate the generation and verification of: 

• Zone Controller and ATS control logic, including routing rules, interlocking behavior and operational constraints 

• Movement authority and speed profile logic, consistent with moving block or quasi-moving block CBTC principles 

• Interface and communication message definitions, ensuring correctness of onboard-trackside and ATS-DCS interactions 

This automation significantly reduces manual engineering effort, enhances functional safety and accelerates delivery of highly reliable, digitally verified CBTC systems – supporting India’s transition toward a fully automated, safety-assured metro network. 

About Prover 

Prover is a global leader in signaling design automation and formal verification, helping rail operators and suppliers deliver safe, certifiable signaling systems faster and more efficiently. Our tools are deployed worldwide to automate the design, verification and validation of rail control systems. 
Learn more at www.prover.com. 

About BHEPL

BHEPL (Bharat Heavy Engineering Private Ltd) is an Indian engineering company specializing in railway signaling, electrification and automation. With a strong presence in national infrastructure projects, BHEPL delivers end-to-end solutions to Indian Railways and metro systems, contributing to India’s ongoing modernization efforts. 
Learn more at  www.bhepl.com. 

Inlägget Prover and BHEPL Partner to Bring Signaling Design Automation to India dök först upp på Prover - Engineering a Safer World.

Exploring the interlocking’s full lifecycle

Our goal was to help them explore the entire lifecycle of a railway interlocking system, from layout design and safety requirements to formal verification and testing, all supported by Prover Studio and Prover iLock. The challenge was to build a complete railway line with 7 interlockings, prove the safety of the line, and simulate the behaviour of the whole system.

We began by introducing the fundamentals of railway signalling and explaining what an interlocking is. Equipped with this knowledge, the students first debugged an existing interlocking system following fundamental signalling principles by using formal verification.
Once confident, they defined and verified new safety requirements, created test cases, and implemented a manual release feature, addressing design, safety, and testing aspects within a single, integrated workflow.

Impressive Progress and Collaboration

We extend our warmest thanks to the CentraleSupélec students for their commitment and enthusiasm throughout the week. They impressed us with how quickly they are handling our tools, modelling language, and dealing with the complexities of the railway domain. Special thanks also go to Idir Ait Sadoune and the teaching team for renewing their trust in us again this year.

At Prover, we firmly believe that introducing formal methods and signalling engineering to the next generation of engineers is essential for building safer and more reliable railway systems. We look forward to seeing these talented students again, in the railway industry or the field of formal verification, as they help engineer a safer world.

Inlägget CentraleSupélec students taste Signal Design Automation dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Verification & validation

As rail control software gets more complex, the real challenge is to ensure that implementations meet safety and functional requirements efficiently and convincingly. EN 50716 (the successor to EN 50128/EN 50657) sets the software development and verification expectations for railway applications, clarifying how formal methods and tool qualification contribute to a robust safety case. This session takes a practitioner’s view of applying that framework to real systems and on‑board functions.

We’ll walk through a repeatable assurance workflow: capture requirements as verifiable properties, model behavior in HLL and its sequential extension sHLL, use model checking to explore relevant executions, and establish auditable conformity between specification and implementation. We’ll illustrate the approach using Prover’s toolchain (HLL/sHLL, Prover PSL, Prover Certifier) to make the approach concrete, while maintaining the emphasis on methods, evidence, and governance that can be adopted in any environment.

Agenda:

• EN 50716 in practice. What changed from EN 50128/EN 50657, specifically regarding the role of formal methods within the lifecycle, and what auditors expect in terms of tool classification and evidence.

• A pragmatic formal‑assurance workflow. From property‑driven requirements to HLL/sHLL models, Prover PSL model‑checking, traceability, and preparation of sign‑off evidence.

• Software conformity by proof. How proof‑producing sign‑off with a T2‑qualified engine (e.g., Prover Certifier) demonstrates alignment between specification and implementation for SIL‑classed applications.

• Quality & efficiency gains. Ways to shorten verification cycles, raise coverage beyond testing, and catch defects earlier—without disrupting your current development process.

Yes please, send me the recording!

Speakers

Benjamin Blanc
Solutions Manager at Prover

Inlägget Software formal verification in the context of CENELEC EN 50716: from model to sign-off verification dök först upp på Prover - Engineering a Safer World.

Imagine a train weighing thousands of tons, moving at 200 km/h – and hundreds operating simultaneously across a network, guided only by software and signals. When everything works as intended, operations are seamless. However, if something goes wrong, the consequences can be catastrophic, including lives at risk, infrastructure damage, and service disruption.

Over the past decades, railway control systems have grown increasingly complex. Testing and manual reviews remain essential, but they can no longer ensure full coverage. The number of possible system states is simply too vast. In many cases, billions of combinations that no test suite could ever exhaust. Traditional methods show the existence of bugs, not their absence.

A new era of railway safety verification

Formal Safety Verification (FSV) is a breakthrough approach that utilizes mathematical proof to ensure a system meets its safety requirements in every possible state. Instead of relying on selected test cases, engineers use models and automated verification tools to prove that no unsafe scenarios can occur exhaustively.

Prover’s Solution Formal Safety Verification makes this process industrially viable. It integrates proven formal methods with efficient tooling to verify complex rail control systems at scale, across all Safety Integrity Levels (SIL 0-4) and in compliance with CENELEC standards EN 50716, EN 50126, EN 50128, and EN 50129.

How safety is usually handled

In EN 50126, safety is an independent process that starts with the identification of all potential hazards that can affect your system. Then, provided the likelihood of these risks is high enough, some mitigation is added as an extra requirement to the development of the system, with a dedicated SIL level.

For instance, a function of the control system will be tagged as SIL4, and the means to address this criticality is to develop this function following the EN 50716 process, with testing and reviews, and even formal proof to verify that the requirements are correctly implemented. The safety case then collects evidence that the whole process covers these risks, by the book.

From traditional testing to formal proof

Traditional verification relies heavily on reviews and test campaigns that are both labor-intensive and prone to human error. Engineers spend valuable time ensuring coverage and tracking potential corner cases: test scenarios are based on the experience or imagination of the test team.

Formal Safety Verification changes the paradigm. Instead of ensuring that the requirements are implemented as they should be, the new process begins with the hazards themselves, utilizing a model of the system design in a formal language to create a digital twin of the control system. Automated model checkers then verify that the model fully satisfies all hazards, independently of their mitigation. If issues exist, they are presented as high-level scenarios, such as train movements or route conflicts, enabling engineers to pinpoint and resolve potential hazards early.

The result: complete coverage, faster verification cycles, and certified safety evidence generated automatically.

Introducing Prover Diagnostic

At the heart of Prover’s solution lies Prover Diagnostic – a packaged, hazard-based formal verification tool that identifies and eliminates potential safety risks before deployment.

Prover Diagnostic integrates:

• Safety properties, derived from system hazards (e.g., collision or derailment scenarios).
• Environment models define real-world constraints, such as the behavior of wayside components (e.g., switch machines), train movement logic, and operational procedures.
• Formal system models, automatically generated or imported from existing design data.

Together, these components form a rigorous verification process in which hazardous states are either proven impossible or clearly reported for review. Prover Diagnostic ensures 100% coverage, a feat no test-based approach can match.

Proven in leading railway projects

Formal Safety Verification isn’t theoretical – it’s field-proven for many years.

• Stockholm Metro uses Prover’s formal methods for both computerized and relay-based interlockings, supported by digital twins for system-level modeling. The approach enables competition among signaling suppliers, reduces lifecycle costs, and ensures consistent safety assurance across upgrades.
• RATP (Paris Metro) applies hazard-based formal verification using Prover tools to validate CBTC systems from multiple suppliers.
• Alstom, one of the world’s largest rail suppliers, integrates formal methods with Prover PSL and Prover Certifier in its global verification process, enabling exhaustive, automatic safety demonstrations from design through implementation.

These projects demonstrate the maturity and scalability of Formal Safety Verification in real-world railway environments. In many cases, the process reveals and allows for the correction of critical bugs missed by traditional testing.

Formal Safety Verification: a summary of the benefits

• 100% safety requirement coverage – mathematically proven, not sampled.
• Early detection of design issues – reducing rework and project delays.
• Certified safety evidence – supporting compliance with international standards.
• Reduced testing and review effort – accelerating delivery while improving reliability.
• Field-proven solution – trusted by leading metros, railways, and signaling suppliers worldwide.

Ready to prove safety with certainty?

Formal Safety Verification empowers rail engineers to deliver provably safe systems – faster and with complete confidence.

Watch the on-demand webinar to learn how Prover’s solution works, explore real-world case studies, and see how formal methods can transform your railway safety verification process.

Watch the webinar recording

Inlägget Formal Safety Verification – How to deliver 100% safe and compliant rail control systems without time delay dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Verification & validation

Recorded on November 5, 2025

At Prover, we address the demand for cost-efficient rail control delivery through Signaling Design Automation (SDA), based on Formal Methods. SDA is also central to the Open Signaling Initiative, promoting open, modular, and interoperable signaling systems. 

With recent advances in AI, we can make SDA more accessible to the rail control community. Adoption challenges often lie in digitizing data, managing requirements, and mastering the technologies. Our goal is to simplify SDA and Formal Methods. In this webinar, we demonstrate how AI enables us to achieve this. 

Agenda:

• The vision for how AI will change the development of safe rail control systems

• Introduction to Signaling Design Automation and Formal Methods

• AI use cases in Signaling Design Automation

• Demonstration: Requirement engineering with AI in Prover Studio

• Interactive Q&A with Prover’s AI and product experts

Yes please, send me the recording!

Speakers

Gunnar Smith
Chief Product Officer at Prover

Fei Niu
AI Innovation Lead at Prover

Inlägget AI, a key enabler for Signaling Design Automation dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Verification & validation

Recorded on September 10, 2025

As digital rail control systems evolve, so do the challenges in validating their safety. Manual testing and reviews are no longer sufficient; they are expensive, slow, and can’t guarantee complete safety. Meanwhile, the cost of missed errors or late-stage discoveries can cause severe project delays or system failures.

Prover’s Formal Safety Verification solution enables a faster, more efficient, and more reliable way to ensure your system meets all safety requirements. It is mathematically proven, highly automated, and compliant with CENELEC standards.

Watch this webinar to learn how formal methods can help you avoid costly project delays, eliminate safety gaps, and streamline your certification process. 

What you will learn:

• Why traditional verification approaches struggle with today’s complex rail systems

• What formal safety verification is and how it works

• How to use model-based development and mathematical proof to ensure 100% requirement coverage

• How Prover’s new solution enables early issue detection, automation, and certified safety evidence

• Real-world results from leading metros, railways, and signaling suppliers.

Yes please, send me the recording!

Speakers

Gunnar Smith
Chief Product Officer at Prover

Daniel Fredholm
Senior Consultant at Prover

Inlägget How to deliver 100% safe and compliant rail control systems without time delay dök först upp på Prover - Engineering a Safer World.

The industry needs to be modernized, standardized, and digitalized. The current processes for developing and maintaining signaling solutions are slow and inefficient. Prover’s approach to SDA, based on digital twins and formal methods, takes automation and efficiency to a new level.

Our new web-based platform Prover Station focuses on critical parts of the design and V&V process, aiding them with digital twins for improved understanding and testing during the development, as well as for training support after delivery. Our extensive experience of formal verification led us to design a workflow for proof projects that will help you succeed in less time and with greater confidence. Progress and obstacles are presented clearly to aid the verification and validation work. We made it easier for non-experts to work with signaling design and for experts to become more efficient and communicate their insights. The result will significantly improve the overall SDA process.

Prover Station is currently available for on-premises installation and in a cloud edition.

Prover Station is a strategic platform that we continue to develop rapidly, aiming to cover the complete process. With capabilities for digital twins and proof projects in place, we now continue to develop what we find most important for efficient SDA projects, such as:

• Creation of digital twin models
• Extensive APIs for integration and automation of tasks
• Third-party contributions that connect Prover Station to other tools
• Data preparation capabilities

“We have leveraged our decades of expertise in Signaling Design Automation (SDA) based on formal methods to build a modern platform that will transform the industry,” says Jesper Carlström, Chief Product Officer at Prover.

Digital twins are a critical success factor for managing signaling design

In the digital transformation era, the ability to create and manage digital twins is becoming increasingly important for organizations in the railway industry. They are now used in model-based tendering, planning phases, design debugging, verification and validation, and post-delivery training.

Working practically with digital twins is a challenge, specifically if large complex systems need to be managed, like a complete railway line.

“The industry needs to be transformed through standardization, digitalization, and interoperability. Digital twins are a critical enabler of this transformation. I’m looking forward to an industry that finally can implement digital twins in real work, developing the signaling solution of the future, which will now be easier with the launch of Prover Station.” Says Anders Lindén, CEO Prover.

Prover Station provides state-of-the-art capabilities for setting up and configuring digital twins. Digital twins allow engineers and operators to understand what they have, to understand what they need to do, and to understand what the results became. You can monitor, analyze, and optimize system performance based on accurate models. By using digital twins, organizations can identify potential issues before they occur, reducing downtime and improving overall system efficiency.

One of Prover Station’s key strengths is its ability to connect multiple digital twins into a single, cohesive aggregate model that provides a holistic view of the entire signaling system, allowing for more effective decision making and system management. The aggregation process and configuration require no user programming.

The use of digital twins in Prover Station is not limited to monitoring and optimization, but also plays a crucial role in system design, testing, and maintenance. Engineers can use these models to try various ideas, helping to ensure that the final system design is robust and capable of meeting all operational requirements. By incorporating digital twin technology into the design process, Prover Station helps organizations achieve greater flexibility, scalability, and resilience in their signaling systems.

Formal methods are the standard methodology for signaling design

Formal methods are becoming more and more popular as the method to ensure safety in the railway industry. In particular, formal verification: you prove using automated mathematical logic reasoning that important safety properties are fulfilled by your system. To work effectively with such proof projects, you need tools that execute proofs and keep track of progress and results.

Prover Station helps you organize your formal verification work in Proof Projects. They allow you to have an overview of the ongoing work, follow progress, understand dependencies and report results. The workflow has been designed based on Prover’s comprehensive experience with success factors for verification and validation work. Engineers who are new to formal verification will appreciate the help to select verification strategies and understand what to do next, while senior verification engineers will discover that it has become easier to communicate ideas to colleagues.

Prover Station supports the entire proof lifecycle, from initial specification and modeling to final proof generation and validation. Prover Station’s capabilities include proving properties and showing why requirements are not fulfilled. This ensures that all logical errors are identified and rectified early in the design process, thereby reducing the risk of costly errors in later stages. Graphical illustrations provide overviews of status and aid in understanding details.

The formal verification process in Prover Station is highly customizable, allowing users to define and enforce their specific safety and performance criteria. The software’s powerful algorithms can handle the most complex signaling logic, ensuring that even the most intricate systems can be verified with confidence. By integrating formal verification into the design process, Prover Station helps organizations meet stringent regulatory standards and enhance their signaling systems’ overall safety and reliability.

Prover Station easily integrates into existing IT Environments

Prover Station can be used in the cloud but is also offered as on-premises software. We continue to expand its capabilities, and at every step, we ensure that it can be used via the web interface and in automated tasks using our APIs. External simulators can be connected via the MQTT protocol or OPC-UA, as can hardware for hardware-in-the-loop testing. If your software or hardware does not support these protocols, it is usually straightforward to develop the necessary adapters.

Conclusion

Prover Station is a comprehensive platform designed to meet the most demanding requirements of the railway and metro signaling industry. With its advanced capabilities in formal verification and digital twin technology, Prover Station empowers organizations to achieve higher levels of safety and reliability in their signaling systems, while also shortening development time. Whether you are involved in proof projects, system design, or ongoing system management, Prover Station provides the tools needed to succeed.

Ready to revolutionize your railway signaling systems?

Experience the power of Prover Station with a personalized demo. Read more about Prover Station here.

Inlägget Prover takes railway Signaling Design Automation to a new level with the launch of Prover Station dök först upp på Prover - Engineering a Safer World.

RECORDED WEBINAR

Verification & validation

Recorded on October 17, 2024

The industry needs to be modernized, standardized, and digitalized. The current processes for developing and maintaining signaling solutions are slow and inefficient. Prover’s approach to SDA, based on digital twins and formal methods, is taking automation and interoperability to a new level using our current tools and expertise.

Railway control systems are interconnected into smaller pieces. Hence it needs to be checked that they are combined properly. Usually, this is done at a very late stage in the process, namely when the system is under verification and validation. With Prover Station, it will become natural to simulate components at an early stage of the process, allowing to ensure performance and to discover unwanted scenarios early.

With the launch of Prover Station as our next-generation platform, we meet the increasing demands of simulation and scenario exploration in the railway industry. And not only is it possible to run predefined scenarios, but thanks to the power of formal methods, it is possible to explore scenarios that you did not even think of.

Agenda:

• The Prover Station platform and roadmap

• Creating and managing digital twin aggregates for testing and training

• Working effectively with proof projects in formal verification

• Simplifying signaling design for beginners and improving expert communication

• Questions & answers

Yes please, send me the recording!

Hosts

Benjamin Blanc
Solutions Manager, Prover

Jesper Carlström
Chief Product Officer, Prover

Inlägget Launch of the next generation Signaling Design Automation platform: Prover Station dök först upp på Prover - Engineering a Safer World.

Verification & validation

Verification and validation are critical processes in rail control projects. Verification ensures that the system meets the specified requirements and design, while validation ensures that the system meets the user’s needs and operates as intended. Both processes involve testing, analysis, and documentation to ensure safety and reliability in railway operations.

In this guide you will learn:

• Achieving safety standards with formal verification

• Advantages over traditional methods

• Impact on verification and validation

• Practical implementation recommendations

Yes please, send me the guide!

Introduction

Guarantee the safety of your rail control system.

When developing safety critical rail control software, achieving compliance with safety standards such as CENELEC EN50128 is a significant part of the project. Traditionally, this involves a number of manual steps such as reviewing verification documents, making test plans and reports and, of course, testing itself.

These activities are typically carried out at a later stage of the project, where delays can significantly impact the overall schedule and any issues discovered are costly to address. Furthermore, the highly experienced staff who have the qualifications needed to perform these tasks are often a bottleneck resource.

The solution is to consider safety, and how it is demonstrated, from the start of the project, and to use more automation throughout the verification process. Much of the work of achieving compliance with safety standards can be replaced with Formal Verification. A technique based on mathematical proofs that gives 100% coverage. Since Formal Verification gives full coverage and is fully automated, not only will it increase safety confidence but it will also help reduce the overall cost for safety assessment.

What you will learn in this guide

In this guide, you will learn how to use Formal Verification to meet prevailing safety requirements with full confidence. All while reducing effort, increasing quality, and reducing the risk for project delays in the process.

On the following pages, we will summarize the safety requirements for rail control software set out by the prevailing CENELEC EN 50128 standard, discuss the advantages of using Formal Verification versus traditional system testing methods, and take a closer look at how Formal Verification impacts the verification and validation process and safety approval in rail control projects. Finally, we will explore how Formal Verification is used in practice and offer some recommendations for the implementation process.

Fill out the form to read the full guide.

Inlägget How to build a solid safety case for your rail control system using formal verification dök först upp på Prover - Engineering a Safer World.

How safe and efficient are your rail control systems? Let’s find out!

Inlägget Cut on-site testing time by up to 50% using formal verification dök först upp på Prover - Engineering a Safer World.