On Monday May 30, Laurent Ferier, our Expert in compilation techniques and domain specific languages, demonstrated the efficiency of the ERTMSFormalSpecs tool to analyze Change Requests in WCRR Milano.
We are publishing below a digest of his presentation. You can ask to download our exhaustive paper HERE.
USING ERTMS FORMAL SPECS TO ANALYZE CR
Subset-026 is a normative document which specifies the EVC behavior. Its size, its structure, and the fact that it is written in natural language lead to interpretation issues. This in turn leads to high costs during requirement management, development and system maintenance.
ERTMSFormalSpecs (EFS) is an open source CASE tool used to formalize ERTMS specifications for onboard units. It manages the entire modeling process from requirement analysis to testing and sets a huge emphasis on traceability: traceability is used to compute metrics, to identify the gaps in the modeling or the tests, and to navigate to and from requirements.
ERTMSFormalSpecs aims at satisfying two contradictory objectives: being understandable by the signaling expert, and being formal enough to be animated. With its 90% model coverage for onboard requirements specified in Subset-026, 027 and 034, we claim that the tool is efficient to model and reproduce real EVC-related situations. This is a breakthrough since it is the first time that the EVC specifications have been modeled and completely traced to that extend. Our purpose is to keep improving coverage, maintain the model and keep it up-to-date with further requirement releases.
A huge amount of Change Requests (CRs) is raised every year by the railway operators for ERTMS. Their handling is performed by several groups of interest: the European Railway Agency (ERA), the ERTMS Users Group (EUG),… but they raise impact and communication problems: since the textual specification cannot be animated, one cannot easily assess the impact of a change on the complete system. Moreover, demonstrating that a proposed solution adequately solves the problem leads to time consuming analysis and meetings.
Our exhaustive paper shows how a real CR can be analyzed using ERTMSFormalSpecs, along with its additional DMI and Scenario Editor visualization tools. It goes from the problem reproduction to the analysis and dynamic visualization of the proposed solutions, a process which is significantly more efficient than paper-based analysis. Using these tools, we expect this to drastically divide the time spent analyzing CRs related to EVC behavior, and to improve the quality of the proposed solutions.
You can ask to download our exhaustive paper HERE.