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 / model checks #44

Closed stanpinteTheSignallingCompany closed 10 years ago

stanpinteTheSignallingCompany commented 11 years ago

in the following note:

"The only verification supported is lexical and syntactical verification, no means are provided to check for example types, domains, or properties."

Incorrect statement. Types, domains are verified by the ERTMSFormalSpecs tool.

Could you please remove that note?

MariellePetitDoche commented 11 years ago

Please to details in your document which kind of verification is provided by the tool and how. Current description "Input verification: First part of the activation cycle. This phase handles verification of the IN variables." in §6.8 of user guides is not enough to understand the verification covers type and domain verification.

stanpinteTheSignallingCompany commented 11 years ago

Now covered by https://github.com/openETCS/ERTMSFormalSpecs/issues/118.