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.

In my last post I wrote about how to write a decent specification on a quite general level. This time, I like to return to the topic, trying to be a bit more specific and tell you something about how we at Prover like to do things. In the Prover Trident Process, the specification of an interlocking is done in four parts: the object model, the generic design specification, the generic safety specification and the generic test specification.

Specifying interlocking software

What is it one needs to specify when specifying interlocking software? Basically, a specification should answer two questions: what and how. The ‘what’ part should tell you what the interlocking should do. In order words, it should specify expected behaviour. The ‘how’ part should tell how this expected behaviour is to be accomplished.

The ‘what’ part – What the interlocking should do

Let’s begin by looking at the ‘what’ part. As we already noted, this is to tell us something about the expected behaviour of the interlocking. To put it simply, the interlocking is expected to allow trains to run in a safe way. If we look closer on this simple statement, we see that it actually contains two parts. The interlocking should allow some things (‘trains to run’) while prohibiting other things (‘in a safe way’). In terms of functionality, it thus makes sense to talk about positive functionality, the things allowed, and negative functionality, the things prohibited.

How does one specify positive functionality? This is nothing else than test cases. For example, if a route fulfills all the requirements for locking and clearing the signal at the beginning of the route, then a request of the route should result in the locking of the route and clearing of the signal. All these test cases are collected in the generic test specification.

What about negative functionality, the things prohibited? Since this is supposed to describe things that are never to happen, it is not practically possible to specify these as test cases. Instead, they are to be thought of as requirements. And since they are to ensure safety, they are actually safety requirements. A typical example could be the following: ‘If a route is locked, then all track circuits that are part of the route should be free of obstacles’. The safety requirements are written down in the generic safety specification.

The ‘how’ part – How the interlocking is to function

With the generic test specification and the generic safety specification, we now have a complete answer to the ‘what’ part of the interlocking specification. What remains is the ‘how’ part. This is done in the generic design specification. It should tell us how the interlocking is to function; how are routes to be locked, signals cleared, switches thrown and the like. In other words, the generic design specification is an implementation of all the functions that are to be present in the interlocking.

So are we done now? Well, not quite. The generic test and safety specifications tells us the expected behaviour of the interlocking, whereas the generic design specification gives an implementation of the interlocking. Hence, they all are supposed to refer to the same thing. The question that remains to be answered is how do we ensure that they do that. Consider route locking, for instance. How do we make sure that the route locking in the generic test specification, the generic safety specification and the generic design specification are all the same? This is where the object model comes into play.

The object model

The object model specifies the types of objects that are present in the interlocking. These can be concrete, representing real railyard objects like track circuits, signals, and switches. They can also be abstract, like routes and local release areas. For each object type, the object model specifies a number of things. The exact list may vary, but it typically includes inputs (which may be categorized into physical inputs and inputs from office system); important states, like ‘locked’ for routes; and outputs, including physical outputs. The main thing is that the object model provides sufficiently rich points of reference to the interlocking so that the other specifications can be written without any further data. It specifies the common concepts of the other specifications.

Although I mentioned the object model last, it is actually the part that should be developed first. Then the generic design, test and safety specifications can be developed independently and in parallel.