ERTMS Solutions has now achieved a long standing objective by completing the full testing of the Subset-076 using ERTMSFormalSpecs (EFS): a fully executable formal model of the Subset-026 specifications. This moreover marks the completion of our contribution to the action entitled “Support to the implementation of ERTMS” of the grant agreement between the Innovation and Networks Executive Agency and the EEIG ERTMS Users Group initiated in January 2015.
According to Action 14 of this agreement, we were committed to develop and maintain ERTMSFormalSpecs, an open source formal modelling toolchain compliant to B3 MR1 and B3 R2 and fully tested against both corresponding versions of the Subset-076. Reports with the errors detected in the Subset-076 should be provided too. This is now done.
ERTMSFormalSpecs : Genesis & Main Features
The EFS project was initiated well before the grant agreement. In fact, about 70% of B3 MR1 were already modeled by July 2015. Indeed, since we develop tools to help the railway industry to design, monitor or control the various ERTMS aspects of infrastructure or onboard units (e.g. BaliseLifeCheck, ERTMSCamCorder, Onboard Monitoring Box) and since the specifications suffer some limitations (natural language, size, completeness, consistency) the need for a runnable version of the specification rose quite soon. Something one can play with, something one can use to get a better understanding, to study corner cases, in a word, to ease specifications analysis.
From the very beginning, EFS was conceived as a tool chain to be used for creating an executable model of the ERTMS specifications. In particular, the user has the possibility to design and play test scenarios. Those are sequences of steps containing Actions and Expectations. Actions are statements which will change the state of the system, like the reception of a Balise Group Message, the acknowledgement of SR mode by the driver. They will be applied at the beginning of the step. Expectations are tests to check the state of the system, e.g. is the current mode FS?, or are the brakes applied? Checks are evaluated at the end of the step.
Test scenarios are valuable tools to check the compliance of your implementation to the specifications. We imported all the Subset-076 test sequences in EFS and executed all of them. We will come back to this later. From a reverse perspective, test scenarios are also used to analyze the specifications, to answer questions such as: How would the EVC react in such a situation?
This specification analysis capacity is even more enhanced in EFS thanks to its Update Mechanism. This mechanism allows to load, in addition to the original model, other add-ons which alter the behavior of the original model and/or add functionalities to it. Those add-ons are typically very small when compared to the original model since they only contain changes, deltas, with respect to it. The time spent to develop them is therefore very limited. Moreover, the original model itself is not changed in any way. Simply unloading add-ons brings back the original behavior. This capacity makes EFS very handy to analyze Change Requests.
ERTMSFormalSpecs : Specific features & achievements
The modeling of both B3 MR1 and B3 R2 are 100% complete. The later was obtained as an update of the first version allowing for a full modeling in a couple of month only.
This modeling uses a Domain Specific Language. EFS names of variables, procedures, ranges like CommunicationSession, HandleLinkingProfile, SendPositionReport, M_ADHESION, should look familiar to any acquainted with the specifications. This really eases the translation of specification concepts and rules into their implemented counterparts, facilitating the modeling process. This also makes EFS implementation easy or easier to understand for people in the business.
EFS also uses a traceability mechanism. As shown on the figure 1 below, the full specification is imported in EFS and its requirements are linked to the model elements which implement them. This is particularly useful as a documentation purpose: how would a specific requirement modeled? Or to indicate to which requirement relates part of the model?
Fig.1 Traceability in EFS
Handy features have been developed on top of traceability to ease the modeling process. Metrics have been added to indicate to what extend the modeling has been completed. We can mark requirements which are not yet linked, not yet fully implemented, or mark the part of the model which implements a given requirement. The later makes it very easy to locate the parts of the model that need to be updated in case a new specification version is to be implemented or a Change Request to be analyzed.
So far, EFS has been used for specifications analysis, typically Change Request analysis, for braking curves independent testing with Thales, for scenario generation with Transurb.
External visualization tools
To ease user interactions with EFS, we also developed two external tools: the DMI and the ScenarioEditor. Both connect to and exchange data with EFS using the Windows Communication Foundations. However, only EFS is responsible of ERTMS computations (braking curves, mode changes) and the other tools are mostly in charge of display.
Fig.2 DMI
The DMI was designed and implemented according to the ETCS ERTMS Driver Machine Interface specification document (ERA_ERTMS_015560 v360). As such, it allows the driver to complete a Start of Mission procedure, acknowledge various information notably. It is also in charge of the display of the Speed and Distance information, planning area, text messages. But again, nothing is directly computed by the DMI, the displayed information is directly read from EFS while only driver’s answers to certain events are sent back to EFS for treatment.
The ScenarioEditor allows the user to design virtual tracks, placing virtual trackside events on it such as BG message reception, and then let the train drive on it. The information sent to EFS is twofold. In one hand, the ScenarioEditor generates OdometryMultiCast messages which simulate train movements. For this purpose, it reads and considers some information from EFS such as the Traction CutOff function status or the brakes status. On the other hand, the ScenarioEditor also sends the trackside events defined by the user to EFS. Many elements can be displayed while playing the scenario and in particular all curves related to Speed and Distance monitoring (notably braking curves, MRSP). Again, this displayed information is directly read from EFS.
Fig.3 ScenarioEditor
In the video below, you see a train starting a mission in Staff responsible mode, then switching to Full Supervision at reception of a Movement Authority.
Modeling in EFS
As already mentioned, the modeling process started by importing the specification into EFS. Our sources were the Subsets 026, 027 and parts of the Subsets 034 and 040. We also considered the Subset-023 and the DMI Start/Stop conditions documents on needs.
The whole specification was then divided into functional blocks, i.e. logical groupings of requirements that form a unit in the model. In most cases, the content of any functional block is also grouped as a collection of requirements in the specification but for the largest blocks, part of the information may be dispatched trough the specification. Modeling per functional block then allowed to keep consistency and ensured the developer to have the full broad picture before proceeding.
Fig.4 Functional blocks examples
Two numbers are associated to each functional block: the percentage of all requirements that this block represents (on the left on the picture) and the amount of this functional block left to implement (on the right). So functional blocks are a dashboard of the model state. Moreover, EFS allows the developer to select and mark all the requirements belonging to a given functional block helping him to figure out what has still to be implemented.
The new specification release BL3 R2 is an iteration on the previous version incorporating many Change Requests. We therefore used EFS’ update mechanism to implement this new version. Accordingly, only the changes with respect to the previous version are modeled in a separate file, the ‘base’ model being kept unchanged and can be loaded without the update as before.
During the modeling process, we sometimes felt the need to add Design Choices to the specification. Those are statements added to the specification in EFS and traced and modeled like all other requirements. They typically come from the following situations:
- Statements of our understanding: e.g. « N_PIG given in each balise of a balise group are unique, even for duplicate balises»
- Imports from other specifications: e.g. For Subsets 023 and 040 we only included the relevant paragraphs, because so little was relevant
- Inferences from many documents: e.g. Hour glass symbol – two design choices based on DMI Start/Stop conditions, DMI specifications (ERA_ERTMS_015560)
- Additions based on Subset-076 testing: e.g. The procedure for RBC-RBC handovers was redesigned many times as Subset-076 test cases illustrated and completed the requirements in Subset-026
We have included 199 design choices, for BL3MR1 and BL3R2 combined. Most of them being common to both versions.
Subset-076 analysis
Susbet-076 test sequences are in nature very similar to the test scenarios presented above. They are described as sequences of steps presenting inputs to be provided to the EVC and outputs to be expected from it. In addition to this, distance, mode and level are provided at the step entrance and exit. Sequences are provided as human readable doc files and computer readable AccessDB files, both containing the same information.
In order to be executed, Subset-076 sequences first needed to be imported from the Access DB file into an EFS textual database. Then, as Steps are expressed in plain English, sequences needed to be translated in sequences of Actions and Expectations executable by EFS. We created a translation dictionary associating Steps’ English sentences (and possibly comments) to sets of Actions and Expectations. In turn, the same translation rules were automatically applied iteratively to several Subset-076 sequences, the translation dictionary being expanded on need during the analysis process. Some situations couldn’t be translated automatically (eg. any time there was contextual information, this couldn’t be got through a simple translation dictionary). Anything unexpected was then handled manually.
Fig.5 Subset-076 sequences import and translation
Once imported and translated, the sequences were executed and analyzed, a sequence being considered as successful when the scenario ran until the end and satisfied all its Expectations. This analysis highlighted many issues in the test sequences. This showed that applying an automated process on the test sequences is of great value. A few shortcomings were also discovered in EFS model and were corrected. To avoid regression, as the model was a few times modified, the analyzed sequences were executed and checked automatically on a daily basis.
Our findings were communicated to the EEIG, the ERA and the laboratories.
Conclusions
We are very proud to have created an executable model of the Onboard Unit specifications, completely compliant to both BL3 MR1 and BL3 R2. Reacting like an EVC would do, it proved to be very useful to assess specifications consistency, to analyze Change Requests and to assess Subset-076 quality.
We warmly thank the Innovation and Networks Executive Agency and the EEIG ERTMS Users Group for supporting this project.
Looking for more information about ERTMSFormalSpecs? Please check out our articles or, feel free to contact us at info@ertmssolutions.com
