Formal Specification

A mathematical description (formalization) of the properties and behavior of a software system.

A mathematical description of the properties and behavior of a software system.

THE IMPORTANCE OF QUALITY SPECIFICATIONS

Specifying your requirements in the tender process is a critical first step.

Of all the steps involved in the tendering process for railway signaling systems, one thing can impact your project the most – your new system’s specifications.

Any errors or omissions in your specifications will impact the later steps in the tender and development process. Mistakes introduced early and discovered late will be costly to correct.

Digital Twin

How to get your rail control project off to a better start.

At Prover we help you getting the specifications right from the start, already at the tendering phase. Getting the specifications right from the start will help you avoid costly mistakes and ensure the right system is built in the first place.

To ensure your specifications are high-quality, we validate them through simulation and formal verification. This is done with our formal methods and the digital twin of your existing and future system.

FORMAL METHODS

How to develop specifications and digital twins using formal methods.

When creating a digital twin of your rail control system, the first step is to specify the requirements for the function and safety of the system. These requirements are then used to define the design specification for the implementation.

An Object Model is also defined, serving as a common interface for the test, safety and design specifications, so that these can be developed independently. The digital twin is then used in an iterative process to validate and refine the requirements.

High-quality and Formal Specifications make it possible to:

Procure the best solution and service for the best price
Efficiently handle change requests and upgrades after commissioning
Minimize risk for project delays
Automatically prove safety

Automate the development process
Validate that the delivered system meets requirements and expectations
Simplify maintenance and upgrades after commissioning

How to Develop Rail Control Software with Signaling Design Automation and Digital Twins

Download guide

References

Prover’s innovative solution bring benefits to many types of Rail Control Projects.

View all

Implementing Prover Trident for SL, Stockholm
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
Our Formal Verification Solution for RATP, Paris
In this project Prover collaborated with RATP in creating a formal verification solution to meet RATP demand for safety verification of interlocking software. RATP had selected a computerized...
Implementing the Prover iLock tool-suite for Canadian Pacific
Class I freight railroad Canadian Pacific (CP) is increasing capacity and consistency in their design and test of interlocking software by using automation tools. In 2010, CP introduced automated...

View all

SOFTWARE SOLUTION

Prover Studio – An Integrated Development Environment for Formal Specifications

Prover Studio is a development environment integrated with the Prover iLock tool that helps you manage, develop and maintain formal specifications.

To Prover studio

How much can you save by implementing Signaling Design Automation?

In this meeting you’ll find out how digital twins and formal methods can help you achieve your rail control projects in less time and lower costs. And 100% secure system.