search

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 / Language / formal or not #33

Closed stanpinteTheSignallingCompany closed 10 years ago

stanpinteTheSignallingCompany commented 11 years ago

there is the following note:

"ERTMS Formal Spec is not a formal language : semantic is not clearly defined thus no formal verification can be done."

1/ Incorrect statement. ERTMSFormalSpecs is a formal language, in the sense that its semantic is 100% defined. Please identify the undefined semantics, if any.

2/ ERTMSFormalSpecs, according to widely accepted Wikipedia definition, is a formal language (http://en.wikipedia.org/wiki/Formal_language#Definition). Could you please remove this note?

3/ Could you please justify why 1 instead of 3 for Formal Language?

MariellePetitDoche commented 11 years ago

A semantic is defined indeed, but not proof of is completeness and consistency is given. Besides, the only use of this semantic described in the documents is to allow the test execution, no mathematical reasoning is defined on the model.

As defined in the document D2.1, D2.2 and D2.4, ERTMS Formal Spec has a formal notation but not mean to formal reasoning on the model : it is a semi-formal language as SysML not a formal one as SCADE, B methods, PetriNets,...

stanpinteTheSignallingCompany commented 11 years ago

1/ Completeness and consistency toward Subset-026 modelled requirements is ensured in ERTMSFormalSpecs by the use of 1/ model coverage by testing, 2/ traceability 3/ review process.

2/ The semantics of both model and test executions are fully defined. Please provide missing semantics if any.

3/ Both Siemens and TWT, assessors of SysML with Enterprise architect, gave a 2 for "Formal language". As ERTMSFormalSpecs has a fully defined semantics for model and test executions, it deserves a 2 for "Formal Language".