ERTMSFormalSpecs covers 100% of Specifications
ERTMS Solutions > Press > ERTMSFormalSpecs covers 100% of Specifications

ERTMSFormalSpecs covers 100% of Specifications

19 January 2017

We are delighted to announce that we have modelled 100% of Subset-026, 027 and 034 (Baseline 3 MR1) onboard requirements using ERTMSFormalSpecs. Ours is the only tool we know of that proposes to the community a complete formal representation of these specifications which

  1. is understandable by signaling experts
  2. can be animated in what-if scenarios.

We are confident about this result because our development process was traceability driven. During each iteration, we identified the requirements that needed development, performed the modelling and simultaneously ensured that traceability links were correctly established. As a result, the model is completely traced, and these bidirectional traceability links can be used for documentation purposes.

According to Laurent Ferier, project leader of ERTMSFormalSpecs, “we quickly encountered cases where design decisions had to be taken during the modelling process, for instance when encountering interpretation issues, or gaps in the specification. Since we had already chosen to focus on traceability, we decided to add these decisions as new requirements, and trace them for documentation purposes.” This is an advantage for the user because these grey spots are clearly identified, and can be easily reviewed if required.

The tool has been used on concrete products. 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 the open source tool ERTMSFormalSpecs in the context of their ERTMS Change Request analysis. More about EUG project

Our next steps are to maintain the model with further requirement releases and to become compliant with Subset-026 version 3.6.0 by March 2017. We are also working towards applying 100% of Subset-076 test sequences to the model.


ERTMSFormalSpecs is a software tool, specifically designed by ERTMS Solutions to formally model and test ERTMS requirements, both for trainborne and trackside systems. The tool includes a railway signaling domain specific software language, a tool chain and a test environment.
Know more about ERTMSFormalSpecs on our website or contact us at

Part of our costs on this activity are covered by a 50% grant from INEA under the Connecting Europe Facility

ERTMS Solutions
Brussels HQ

Tel: +32 2 612 41 70

Fax: +32 2 522 0930
Rue de la Caserne 45

1000 Brussels – Belgium

VAT: 0897.249.802 / European ID-Entreprise ID: BE0897249802

How can we help you ?

By continuing to use the site, you agree to the use of cookies. more information

The cookie settings on this website are set to "allow cookies" to give you the best browsing experience possible. If you continue to use this website without changing your cookie settings or you click "Accept" below then you are consenting to this.