openETCS / model-evaluation

part of WP7: collects the various activities regarding selecting a tool and formal specification for modeling
13 stars 20 forks source link

ERTMSFormalSpecs assessment by Assessor 2 / Main usage of the approach / missing elements #30

Closed stanpinteTheSignallingCompany closed 10 years ago

stanpinteTheSignallingCompany commented 11 years ago

In section C.2 Main usage of the approach, there is the following note:

"elements of methods are still missing to know how to use and integrate the language and tools in a whole development."

Could you please identify precisely the missing elements, or remove the note?

MariellePetitDoche commented 11 years ago

Methodological guides to how to use the language and the tool is not yet provide, for the moment the document list in C3 are only user manuel of the tool and description of the language.

The aim of specifying the model in ERTMSFormalSpec on the project and the link with other activities of the project is not highlight. Besides way to write the model (as for example template for state machine, rules of writing,...) are not defined in the documents. Question raise in the issue : https://github.com/openETCS/ERTMSFormalSpecs/issues/107 has not clear answer on the way to proceed to select definition versus requirement and to justify definition are not modelled.

stanpinteTheSignallingCompany commented 11 years ago

Thank you for your answer.

Regarding how to use the language the ERTMSFormalSpecs toolchain, this is clearly the scope of the document https://github.com/openETCS/ERTMSFormalSpecs/blob/master/ErtmsFormalSpecs/doc/EFSW_User_Guide.pdf.

However, specifying how ERTMSFormalSpecs should be used within OpenETCS and the link of other activities of OpenETCS is outside of the scope of ERTMSFormalSpecs documentation.

How to write the model is fully integrated inside the User Guide, for instance in section 7:

2013-07-01 15_56_52-efsw_user_guide

Regarding issue https://github.com/openETCS/ERTMSFormalSpecs/issues/107, this is not an issue of documentation, but an issue for the SSRS task (which shall among other tasks justify which S026 requirements shall be modelled and which not).