Formal Development

Formal Development

Automating code generation of software systems using formal methods.

The process of creating software systems using formal methods.

Automating software development

There is an easier route to rail control
software development

In the endeavor to develop rail control software that meets demands for efficient rail transportation, both now and in the future, many of today’s infrastructure managers find themselves impeded by a number of frustrating roadblocks.

These include long and unpredictable schedules, a general lack of control over systems, and dominant industry issues such as the current oligopoly of system suppliers who deliver systems without consideration for open standards and interfaces.

Formal methods

Formal development to overcome costly barriers in rail control projects

The process used to overcome the common challenges in rail control software projects is Signaling Design Automation. It is a set of automation tools and processes based on formal methods that can be used to develop software for rail control systems.

Read more about Signaling Design Automation.

Formal methods

SDA integrates formal methods
into an automated development process

SDA combines automation with the tools that formal methods offer to ensure that you can efficiently develop rail control systems and verify that they meet requirements during Verification and
Validation (V&V). The automation tools can be used to your advantage at every phase of the software development process – from establishing requirements to system development and maintenance.

Gain more control over your system and quickly identify issues

Capturing requirements for safely testing undefined system configurations is a key concept in the SDA process. This includes a clear separation of different types of requirements (configuration,
interfaces, safety, and test). SDA also promotes the use of open and standardized component formats and interfaces. As a result, you as an infrastructure manager gain more control over your system and acquire the ability to quickly identify and debug
requirement issues before they become a major problem.

System control

How does formal development work?

Generation of requirements

1. Generation of requirements

Generic requirements for a given type of system are specified and formalized, with a clear separation of design, safety and test requirements. Design, test cases and safety requirements are generated for each application developed.


2. Configuration

The data is split into Generic and Specific configuration data. From there, you can configure the individual signaling system that you are developing. The tool will take care of creating the specific requirements from your specifications for that particular configuration.

Automated verification and validation

3. Automated verification and validation

The safety requirements are formally verified and test cases simulated. Detailed verification and test reports are generated.

4. Code generation

Code generation tools convert your design into software code to be compiled, configured and installed on the computing platform of the rail control system. This is the software that will be executed on the actual system in the field.

Guide digital twins

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


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


Prover iLock – Railway interlocking simulator, document & code generator, and verifier.

The desktop tool for producing fully documented, tested and verified application software for railway interlocking systems.


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.


Mats Boman
Title, Prover

”We can map the complete workings of a unit at the heart of the cycle, look inside it and see what’s going on.”


Mats Boman
Title, Prover

”We can map the complete workings of a unit at the heart of the cycle, look inside it and see what’s going on.”