-
Notifications
You must be signed in to change notification settings - Fork 20
ERTMSFormalSpecs description
ERTMSFormalSpecs
http://www.ertmssolutions.com/ertms-formalspecs/
i.e. to someone that has authority to answer questions on this tool and that can answer promptly; it can be an alias
Stanislas Pinte [email protected] Laurent Ferier [email protected] Svitlana Lukicheva [email protected]
- Subset-026 Modelling
- Subset-026 Model testing
- Subset-026 Model verification
ERTMSFormalSpecs provides a domain-specific language, designed to express the ERTMS specification in a concise and verifiable formal representation. It is understandable by domain specialists while retaining the ability to be translated to executable representations by fully automated means.
http://www.ertmssolutions.com/files/ERTMSFormalSpecs_WCRR2011.pdf
http://www.ertmssolutions.com/files/UsingERTMSFormalSpecsToModelBrakingCurves.pdf
- Download installer or sources from Github
- https://github.com/openETCS/ERTMSFormalSpecs
- https://dl.dropbox.com/u/86354232/ERTMSFormalSpecs_Setup_0.9.exe
- Execute the installer in src/Installer/release
- Click on the EFS Workbench shortcut
- Pick a requirement and … go
User guide: https://github.com/openETCS/ERTMSFormalSpecs/blob/master/ErtmsFormalSpecs/doc/EFSW_User_Guide.pdf
Language reference: https://github.com/openETCS/ERTMSFormalSpecs/blob/master/ErtmsFormalSpecs/doc/EFSW_Technical_Design.pdf
Commercial support available from ERTMS Solutions. Contact [email protected] for support pricing.
ERTMS Solutions is in operation since 10 years, is profitable, and has support contracts for up to 2013 (for instance with INFRABEL, belgian infrastructure manager). Therefore, ERTMSFormalSpecs can be supported in the long term.
- Understandable by domain specialists
- Executability
- Open-source
- The ability to model all Subset-026 + Subset-076 artifacts rather than being limited to a convenient but pointless selection of facets as provided by these documents
- Braking curves verified with ERA reference model
ERTMSFormalSpecs language. See full language description here: https://github.com/openETCS/ERTMSFormalSpecs/blob/master/ErtmsFormalSpecs/doc/EFSW_Technical_Design.pdf
The following reports are available from the ERTMSFormalSpecs workbench:
- Specification coverage report
- Dynamic tests coverage report
- Data dictionary report
All these reports are fully document in the ERTMSFormalSpecs User Guide.
The main output of the ERTMSFormalSpecs is its model itself, that can be transformed in lower level source code to be compiled on a target EVC platform.
Transformation from model to source code is as of today out of the scope of the ERTMSFormalSpecs workbench.
No restrictions known today. Full list of known bugs, issues, improvement requests available under GIT repository: https://github.com/openETCS/ERTMSFormalSpecs/issues?state=open
The ERTMSFormalSpecs workbench is used to manually model the Subset-026 in the ERTMSFormalSpecs language, and to write functional tests for the various parts of the model.
As the ERTMSFormalSpecs language is designed to be as close as possible to the Subset-026 artifacts, the required expertise level is a good understanding of the Subset-026 itself.
No further specific computer programming background is needed.
The ERTMSFormalSpecs workbench is currently using the latest .Net framewok as a platform.
An installer is available for the windows platform, and should wait out of the box, without any installation prerequisites. (See download and install section above).
An Eclipse porting effort has started, inside the ERTMSFormalSpecs repository:
https://github.com/openETCS/ERTMSFormalSpecs/tree/master/workspace
This porting effort currently enabling the export of the complete ERTMSFormalSpecs model under an EMF model-based repository, editable under eclipse.
Industrials need to maintain some traceability between source documents and deliverables, for certification purposes, as well as for maintenance and evolution purposes. Does the tool provide such traceability, or does it integrate in such a way that the traceability is maintained in a satisfactory way (notably WRT CENELEC requirements)?
Traceability was at the core of the ERTMSFormalSpecs design principles. The ERTMSFormalSpecs workbench enables bi-directional traceability between the Subset-026 and the model and between the Subset-026 and the functional tests.
Complete traceability matrixes are provided inside the Specification coverage report (See above).
can the tool be used by a team working on different fragments of the model? is there a support for versioning?
As of today, the ERTMSFormalSpecs stores its model in a flat XML file, put under GIT versioning.
This is suitable for small models and small modelling teams, however, for larger models and larger modelling teams, a model-based repository is highly recommended.
An Eclipse porting effort has started, inside the ERTMSFormalSpecs repository:
https://github.com/openETCS/ERTMSFormalSpecs/tree/master/workspace
This porting effort currently enabling the export of the complete ERTMSFormalSpecs model under an EMF model-based repository, editable under eclipse.
Currently, there are no blocking issues preventing ERTMSFormalSpecs to be used inside a SIL4 development for an ERTMS OBU, in the context of model-based development.
All issues are recorded on the ERTMSFormalSpecs repository: https://github.com/openETCS/ERTMSFormalSpecs/issues?state=open
An independent ISA audit is underway, to assess suitability for SIL4 development for an ERTMS OBU, and list all the gaps that need to be filled in order to use ERTMSFormalSpecs for that purpose.
People or parties who have developed this and are currently driving the project including their affiliations
- ERTMS Solutions team (http://www.ertmssolutions.com/profiles/headquarters/)
- Eclipse source team (todo)
Latest version available on https://github.com/openETCS/ERTMSFormalSpecs/
Yes, EUPL.
All software needed is either free to use or under an EUPL compatible license.
An Eclipse porting effort has started, inside the ERTMSFormalSpecs repository:
https://github.com/openETCS/ERTMSFormalSpecs/tree/master/workspace
The ERTMSFormalSpecs model is currently available as a flat XML file, with fully defined semantics, therefore transformable to any other format.
Esterel technologies has confirmed the feasability of an automated ERTMSFormalSpecs-to-SCADE model transformation.
ERTMS Solutions has also assessed the feasibility of ERTMSFormalSpecs-to-Matlab automatic model transformation.
No existing industrial usage as of today. ERTMSFormalSpecs is a new approach for ERTMS OBU Baseline 3.
- Model completion is ongoing by ERTMS Solutions, to reach 100% of Subset-026. Today (may 2013) at 37%.
- Eclipse port of the ERTMSFormalSpecs workbench is ongoing.