ERTMSFormalSpecs (EFS) is a workbench used to model and animate ERTMS specifications for onboard units.

The whole modeling process, from requirement analysis to testing, is made easy thanks to its functionalities and graphical interface. Furthermore, EFS sets a huge emphasis on traceability to easily navigate from the requirements to the model and backwards. Thanks to the traceability, we can compute metrics and identify gaps in the model and tests.

 

It includes 100% of Subset-026 ERTMS Business Logic, allowing you to:

    • Test your EVC
    • Validate Subset-026 change requests
    • Perform early-stage development and validation of operational test cases

 

This workbench satisfies two contradictory objectives: being understandable by the signaling expert and being formal enough to be animated.

It includes a DMI window showing the model state and a Scenario Editor which helps defining and playing the scenarios.

With its 100% model coverage for onboard requirements specified in Subset-026 and 027, we claim that the tool is efficient to model and simulate real EVC-related situations.

ERTMSFormalSpecs

Our best references:

  • Thales Transportation Systems GmbH uses ERTMSFormalSpecs to verify that the braking curve computation corresponds to the specification. Read the whole story here.
  • ERTMS Users Group (EUG) used ERTMSFormalSpecs in the context of their ERTMS Change Request analysis. More about EUG project
null

Displays the model state, according to DMI specification

null

Eases the creation of specific scenarios with the ERTMSFormalSpecs Scenario editor

null

Static analysis and reproduction using the Scenario Editor

“ERTMS Solutions has demonstrated the usefulness of their tool, ERTMSFormalSpecs, and the quality of their service. Their expertise in breaking curves is another major element, which convinced us to sign this contract with them. We are convinced that ERTMSFormalSpecs will boost our OBU testing process, provide us large costs and time savings, and increase the transparency of our testing process, towards our ERTMS customers”
thales

ERTMS Users Group (EUG) chose the ERTMSFormalSpecs

In the context of their ERTMS specifications change requests, ERTMS Users Group (EUG) chose the ERTMSFormalSpecs. This video explains how to reproduce and visualize an ERTMS Change Request using ERTMSFormalSpecs.

ertms-group

OTHER PRODUCTS

omb-3d

Onboard Monitoring Box

The Onboard Monitoring Box (OMB) is a passive acquisition and monitoring device, developed by ERTMS Solutions.

ERTMS TrackCircuitLifeCheck

TrackCircuitLifeCheck

The TrackCircuitLifeCheck is a versatile measurement instrument that facilitates track circuit maintenance and is usable on both diagnostic and commercial trains.

ERTMS BaliseLifeCheck

BaliseLifeCheck

The BaliseLifeCheck is a preventive balise measurement instrument that can be used on both diagnostic and commercial trains.

OTHER PRODUCTS

omb-3d

Onboard Monitoring Box

The Onboard Monitoring Box (OMB) is a passive acquisition and monitoring device, developed by ERTMS Solutions.

ERTMS TrackCircuitLifeCheck

TrackCircuitLifeCheck

The TrackCircuitLifeCheck is a versatile measurement instrument that facilitates track circuit maintenance and is usable on both diagnostic and commercial trains.

ERTMS BaliseLifeCheck

BaliseLifeCheck

The BaliseLifeCheck is a preventive balise measurement instrument that can be used on both diagnostic and commercial trains.