
Of all the steps involved in the tendering process for railway signaling systems, writing the specifications that you will later hand over to suppliers is one of the most consequential when it comes to determining how smooth and successful the rest of your project will be.
Here, we will explain how you can succeed in establishing quality specifications at the start of your rail control project by developing a digital twin using formal methods.
Why having quality specifications in the tender phase matters
Clearly specifying your needs, requirements, and expectations is a critical first step in the tendering process. Any errors or omissions in your specifications will have an impact on the later steps in the tendering and development process. And since they were introduced early and discovered late, such errors will be costly to correct.
Common specification issues:
- Incomplete: Specified requirements fail to mention necessary parts of the system or lack sufficient details
- Inconsistent: Specified requirements are contradicting, making realization impossible
- Incorrect: Specified requirements are simply wrong
Taking the time to ensure your specifications are as complete, consistent and correct as possible—not to mention easy to read and understand by suppliers—will help you avoid these issues and prevent the delays and increased costs associated with fixing them later on.
A digital twin makes it possible to validate requirements and spot specification issues upfront
Taking the initiative to create a digital twin at the start of your rail control project before tendering begins enables you to formulate and evaluate more clear and precise requirements for your rail control system. It will also help you ensure that these requirements can be realized in an actual system, and that they are verifiable.
Beyond the tendering process, a digital twin can advantageously be used throughout the lifecycle of your rail control system to reduce costs related to upgrades or the addition of new features during the maintenance phase.
Benefits of using a digital twin during tendering:
- Simplified procurement processes
- More efficient validation and verification process
- Reduced risk of misunderstandings and project delays
- More predictable delivery schedules and costs
- Less time needed for costly on-site tests
- Minimizes the risk of error discovery late in the procurement process
- Easier to accurately gauge whether systems comply with requirements
How to develop the digital twin using formal methods
The digital twin is best developed in an iterative, test-driven, and agile process consisting of three basic steps. Using formal methods enables the development of specifications, digital twins, and actual systems, through the use of a set of automation tools and processes called Signaling Design Automation (SDA). Being formal, such methods offer enough detail in order to be analyzed for completeness, consistency, and correctness.
1. Gather and analyze input
The process starts with an analysis of the needs and information available, which helps define the test and safety requirements on a high level. Tender requirements, use cases, legacy systems, applicable standards, interfaces, rules, regulations, and project scope all provide input to this task.
2. Formulate requirements and define the object model
Formulate the test and safety requirements in natural language using an Object Model that defines the objects in the system and how they interact. The test and safety specifications are then used to define the design specification, for the implementation of the system. The specifications are formalized so that they can be interpreted by automation tools for configuration, design, implementation, testing, and verification.
3. Configure your applications and validate the requirements
Specify the configuration data that will be used to create instances, or Specific Applications, of the Object Model. The formalized requirement specifications are then validated with formal verification and simulation using the Specific Applications. Specifications are then updated based on these results, in an iterative and agile process.
Questions? Book a meeting with us to learn more about how to secure high quality specifications for your rail control project.

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

Learn more about how to develop specifications with Digital Twins
Fill out your information here.
More News & Articles
Explore how Prover is revolutionizing railway signaling with AI and formal methods. Discover Prover Labs: a hub for innovation, collaboration, and shaping AI-driven automation for enhanced safety, efficiency, and precision in signaling design.
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.