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 allowing to easily navigate from the requirements to the model and backwards. Traceability allows to compute metrics, identify gaps in the model and the tests.
ERTMSFormalSpecs includes 100% of Subset-026 ERTMS Business Logic, allowing you to:
- Test your EVC
- Test and validate Subset-026 change requests
- Perform early-stage development and validation of operational test cases
ERTMSFormalSpecs aims at satisfying two contradictory objectives: being understandable by the signaling expert and being formal enough to be animated. It is complemented by 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.
The tool has been used on concrete projects. 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
