Readibility issues in Event B model

[MERCEmentre]

When reviewing Event B model, I found the textual explanation well done and necessary. However I had issues to link the textual explanations with the formal text, especially the complex parts like §5.10.

Moreover, I think the formal model should be as much as possible self explanatory.

I would suggest to give explicit names to invariants and guards. Instead of inv1, inv2, ..., use references to SRS paragraphs and covered properties (e.g. 3_5_3_7_part_of_start_of_mission).

I would also suggest to use such explicit names into the body of the textual explanations surrounding the formal parts.

[mgudemann]

This is a good suggestion and we will add this.

TODO:

• update doc with reference to ReqIF
• reflect requirements in labels

There is a direct link to the ReqIF file in the Rodin project, with links from the requirements to the Event-B artifacts which implements it. This requires the ProR plugin to be installed.