Purpose
To translate Trafikverket regulations/signalling principles into formal requirements and to increase the knowledge and know-how of formal methods at Trafikverket.
Client
Infrastructure Manager: Trafikverket (The Swedish Transport Administration)
Signaling system
Building formal competence for safer and smarter railway signaling
What did we do in forms of technical solution?
Short intro of the project
The project focuses on converting Trafikverket’s signaling regulations (TRVINFRA) into formal requirements to enable digitalization and automation within railway signaling. It is a continuation of earlier work where Prover demonstrated how signaling rules could be expressed in formal logic and verified using model-based tools.
What was the purpose?
The aim is twofold:
- To translate Trafikverket’s signaling principles into formal requirements, ensuring that the regulatory framework is unambiguous, structured, and ready for use in design and verification workflows.
- To build Trafikverket’s internal competence in formal methods, so the organization can manage, maintain, and extend formalized requirements in the future.
How did we resolve the issue?
Prover contributed expertise in formal methods and tool configuration, guiding Trafikverket in structuring and formalizing requirements using the open HLL language. Workshops and training were held to teach formalization techniques, and example requirements were implemented and validated using Prover iLock. A process for managing and maintaining formal requirements was established, including a governance and documentation plan for future use.
What was the result of the project?
The project contributes directly to Trafikverket’s long-term digitalization goals by introducing a methodology that increases safety, reduces ambiguity in signaling regulations, and improves efficiency in design and verification processes. The collaboration between Prover and Trafikverket also establishes a foundation for future projects involving automated signal verification.
Related project references
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
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...
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...
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.
Purpose
To translate Trafikverket regulations/signalling principles into formal requirements and to increase the knowledge and know-how of formal methods at Trafikverket.
Client
Infrastructure Manager: Trafikverket (The Swedish Transport Administration)
Signaling system
Building formal competence for safer and smarter railway signaling
What did we do in forms of technical solution?
Short intro of the project
The project focuses on converting Trafikverket’s signaling regulations (TRVINFRA) into formal requirements to enable digitalization and automation within railway signaling. It is a continuation of earlier work where Prover demonstrated how signaling rules could be expressed in formal logic and verified using model-based tools.
What was the purpose?
The aim is twofold:
- To translate Trafikverket’s signaling principles into formal requirements, ensuring that the regulatory framework is unambiguous, structured, and ready for use in design and verification workflows.
- To build Trafikverket’s internal competence in formal methods, so the organization can manage, maintain, and extend formalized requirements in the future.
How did we resolve the issue?
Prover contributed expertise in formal methods and tool configuration, guiding Trafikverket in structuring and formalizing requirements using the open HLL language. Workshops and training were held to teach formalization techniques, and example requirements were implemented and validated using Prover iLock. A process for managing and maintaining formal requirements was established, including a governance and documentation plan for future use.
What was the result of the project?
The project contributes directly to Trafikverket’s long-term digitalization goals by introducing a methodology that increases safety, reduces ambiguity in signaling regulations, and improves efficiency in design and verification processes. The collaboration between Prover and Trafikverket also establishes a foundation for future projects involving automated signal verification.
Related project references
In signaling design automation projects, we start by developing a digital twin of your existing, future, and conceptual systems.
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...
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...
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.
+46 (0)8 617 68 00