ERTMSFormalSpecs assessment by Assessor 2 / Main usage of the approach / model verification capabilities

[stanpinteTheSignallingCompany]

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

"For verification, it is dicult through the document to understand what is verified. It is verifications are those provided by the tool as lexical or syntax verification. I have not find other kind of verification as type or coverage. How to verify the model in a more general way (indeed that the model specifies well the informal specification) is not describe in the documents."

This is an incorrect statement. ERTMSFormalSpecs provide verification through its User Interface, through traceability and through testing and coverage analysis. The documentation also clearly covers how to verify the model in a general way.

Therefore, could you please

1/ justify why 1 instead of 3 for Verification?

2/ Justify why 1 instead of 3 in section C.8 Main usage of the tool, for model verification

3/ identify, if any, missing documentation items?

[MariellePetitDoche]

"Verification" occurs 5 times in the "User guide": §6.2.2.2 is a mark for review process §6.8 could you give details of the verification done on the input ?

According to system and software engineering, verification can have a very large meaning as described in the VnV plan of WP4. In EN50128 Table A5, A12, A13, A19, A21,... give indication of what can be verified.

If verification artefacts are provided, a dedicated section on this topic with detailed mechanisms of verification in the User guide, will be very useful.

[stanpinteTheSignallingCompany]

Thanks for your suggestion:

"If verification artefacts are provided, a dedicated section on this topic with detailed mechanisms of verification in the User guide, will be very useful."

We recorded it in an issue: https://github.com/openETCS/ERTMSFormalSpecs/issues/118 for later implementation.

Regarding "§6.8 could you give details of the verification done on the input ?", this is a technical verification made by the ERTMSFormalSpecs toolchain during model execution, not a verification in the V&V meaning.

Still, considering the existing documentation and the verification performed by the ERTMSFormalSpecs toolchain, we think a fair assessment would be "2 recommended, adapted (with light improvements if necessary) weakly accepted" instead of "1 weakly recommended, adapted after major improvements, weakly rejected". It seems to be mainly a documentation problem. A documentation issue should not lead to a score of 1 in that context.