openetcs / model-evaluation Goto Github PK

in the following note:

"For example, formal language dedicated to software design as Scade or Classical B, how to structure the model and to define its architecture is an important part of the language, to allow the design of e cient software. i do not see how to link the structure of an ERTMS Formal Spec model closed to SRS to the one of a software."

Could you please remove this comment? ERTMSFormalSpecs doesn't include a software generator, and therefore, the structure of the model can be decoupled from the structure of the software.

When I open the project in GPS 5.1.1 I get the following warning:

default.gpr:1:9 warning: object directory "obj/" not found

when trying to execute "Prove All" or "Prove Root Project" I get the following error message with gnatprove (version "2012 (20120509)")

gnatprove -P/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/default.gpr --mode=prove --ide-progress-bar
Phase 1 of 3: frame condition computation ...
Phase 2 of 3: translation to intermediate language ...
+===========================GNAT BUG DETECTED==============================+
| GPL 2012 (20120509) (i686-pc-linux-gnu) Program_Error gnat2why-decls.adb:626 explicit raise|
| Error detected at a-chtgbk.adb:30:1 [a-cfhama.adb:83:4 [com_map.ads:31:4]]|
| Please submit a bug report by email to [email protected].               |
| GAP members can alternatively use GNAT Tracker:                          |
| http://www.adacore.com/ section 'send a report'.                         |
| See gnatinfo.txt for full info on procedure for submitting bugs.         |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact gcc or gnatmake command that you entered.              |
| Also include sources listed below in gnatchop format                     |
| (concatenated together with no headers between files).                   |
| Use plain ASCII or MIME attachment.                                      |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/src/com_map.ads
/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/obj/gnatprove/GNAT-TEMP-000001.TMP
/users/gudemann.home/tmp/model/tmp/model/GNATprove-MERCE/src/data_types.ads

compilation abandoned

   compilation of com_map.ads failed

gprbuild: *** compilation phase failed
gnatprove: error during translation to intermediate language, aborting.

How can I proceed? Dows the error depend on the first warning?

David,

you have decided to drop the Why3 model.
I think it will be nice to have a short explanation of why you think this tool is not convenient for the OpenETCS project.

Maybe this tool can be take in consideration for VnV activities.

I have a Question concerning 3.13.6.2.1.5

According to special track conditions several special brakes must not be used.

Start, Length and end of the track conditions are described in Messages, but there is no information, how long they should be regarded. In my understanding it should be also taken into account in the whole train length, as it is done in for example at the gradients, because there are no assumptions about the position of the special brake.

Am I reading the SRS wrong or is this a spec issue ?

kind regards

Benjamin

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

"The tool allow the generation of some reports as data dictionary, specification
issues or coverage reports, but no element to understand how the system works in themodel. The current produced elements are not su�cient for a design process."

1/ Incorrect statement. The User Guide explains how the model is built, and has received positive feedback from the industry, from a model-based design perspective.

2/ Please justify why 1 instead of 3 for Documentation. Please identify missing documentation items.

From ProR requirement table, how can I open the link to see the corresponding part of the B Model?

Justify why 2 instead of 3 for documented, as ERTMSFormalSpecs is 100% documented (every feature, how to use, and 100% of language and semantics).

Tool manual (D.2.6-01-42.02)

why 2 instead of 3? We injected a lot of effort into the documentation, and we don't want to receive a 2 without a list of open docu. issues.

Could you please increase your note, or provide a full list of documentation issues?

Justify why 1 instead of 3 for scalabality, whereas ERTMSFormalSpecs already covers 44% of subset-026, and is therefore proven scaleable.

As CEA is a major participant to the WP7 workpackage.
+1

Proposition of contribution for a new model in SystemC / UPPAAL

+1

Justify why 1 instead of 3 for "easely translateable to other languages", whereas it has been assessed as 3 by other assessor, Alstom, and you have provided no justification

Criterias should be quantified

If we are to take a decision on methods and tools, it must be on an objective base, i.e. compliance on the criterias.

That compliance must be quantified somehow (for instance rated on a scale x/100). That rating has to be justified, so that it can be assessed by others.

Of course, we can decide to give different weight to Different criterias, and even to combine languages and tools to obtain a best-of-breed method (for instance, ERTMSFormalSpecs doesn't include formal proof -> if combined With another approach enabling proof, it could score more).

Looking forward to your feedback, I wish you an excellent evening.

Very kind regards

Stan

Cooperation of tools (D2.6-02-076)

1 unjustified. The model is stored in XML file format, and there is already an interaction with Eclipse toolchain implemented, by exporting the full ERTMSFormalSpecs model to EMF repository.

Could you please update your quotation for:

• Cooperation of tools (D2.6-02-076)
• Tool chain integration

we don't agree with 1....the model can be verified through:

• review of specifications and model side-by-side
• testing of model
• traceability

Portability to operating systems (D2.6-02-075)

1 unjustified. The tool should be able to run on Mono.Net, available for linux.

Could you please upgrade your note, and point to the fact that issue https://github.com/openETCS/ERTMSFormalSpecs/issues/113 tracks this question?

In current Event B formal model, there are not traceability to the SRS. How to you plan to handle this part?

Scalability

The note of 1 unjustified, especially regarding the existing 44% of subset-026 implemented.

Could you please change from 1 to 3?

"Is there any document to describe this translation from ERTMSFormalSpecs
to an another language ?"

This is now tracked by issue: https://github.com/openETCS/ERTMSFormalSpecs/issues/112

Could you please add in your evaluation that this issue is tracking your question?

In the following note:

"It is not clear if the test or the model are executed."

Both are executed. the tests are made up of actions on the model variables and expectations on these variables, but the model is executed during the tests.

Could you please read the documentation regarding testing, and point to any unclear statement or missing explanation in the documentation?

The current formal model covers a little part of the SRS (e.g. §3.5.3). How do you plan to cover the whole SRS with Event B? Through several small models, each one covering a subpart of the SRS? Through other means?

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

"For verification, it is di�cult 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?

Please vote for Lukas Ladenberger (https://github.com/ladenberger) from formalmind who is collaborating on the requirements engineering (ProR plugin) integration with Rodin.

This question was raised in munich workshop.

https://github.com/openETCS/model-evaluation/blob/master/Munich_20130416_minutes/Minute%2020130416%20WP7%20evaluation%20matrix.pdf

Justify why 0 for "executable directly", whereas with one click in the tool the model can be executable. Executing the tests do execute the model. The other assessor gave a 3.

I have installed Rodin (v2.7, with recommended tools) and following Matthias documentation (https://github.com/openETCS/model-evaluation/blob/master/model/B-Systerel/Event_B/rodin-projects-github.pdf), I can see the Event B project inside Rodin (inside the "Event-B Explorer" panel).

I can individually open each machine. So far so good.

However, how do I generate Proof Obligations for the model. Is there a specific way to open the model inside Rodin?

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?

there is the following note:

"But this way do not allow to have a really modular design : all the data are stored in the same database, and not clear share of function is provide to allow the design of module in an independent way."

Incorrect statement. Modular design can be achieved by using Namespaces, functions, structures, etc (all typical artifacts of modular languages). The fact that all the model is stored in the same database is not related to modularity.

Justify why 1 instead of 3 for Modular Language. Identify missing documentation items, if any.

Open, collaborative process to establish the evaluation matrix

I understand you have started to work on the matrix, however, all stakeholders of the project should be allowed to participate in the drafting and review of this matrix.
This matrix should not be presented in the Munich workshop, without having being discussed on the WP2, WP3 and WP7 mailing list.

I therefore think that this matrix should be put in GIT in the https://github.com/openETCS/model-evaluation repository, as a .tex versioned-control document, So that we can collaboratively contribute, review and comment. (Maybe it is already the case, sorry if I missed it).

Could you confirm that it shall be the case?

there is the following note:

"Concerning management of requirement justification and traceability to exported
requirements, the current model do not show how this can be systematically covered."

Incorrect statement. The ERTMSFormalSpecs toolchain allow for complete traceability, and provide complete tooling support to enforce this traceability.

Justify why 1 instead of 3 for "Management of requirement justification" and "Traceability of exported requirements"

Criterias should come from WP2 requirements, listed in https://github.com/openETCS/requirements/blob/master/D2.3/Synthesis/req_synthesis.tex

I don't understand why the criterias should come from other sources (report on methodologies, for instance). Criterias should be based on requirements.
These requirements can come from WP2 requirements list (req_synthesis.tex) or other applicable standards like EN50128.

Especially after the collaborative work that has been done around WP2 req_synthesis document. --> This should be the most important input for the matrix.

However, not all EN50128 requirements are applicable on the language and toolchain, and therefore not all requirements should be taken into account in the evaluation matrix. The report from Merlin should provide a starting base for this -> extract the EN50128 requirements that have been judged applicable on language and tools, and insert them in the matrix.

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?

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.

there is the note:

"Standardization is poor due to no methodological guide to apply the approach"

Incorrect statement. Standardization means documentation support, public availability, etc.

Could you please remove the note, or provide due justification?

ERTMSFormalSpecs has good documentation support, including methodology for its intended scope, which is modelling the Subset-026

Could you please justify why 1 instead of 2 or 3?

Dear all,

Could you please vote for my colleague https://github.com/LaurentFerier
to be elected as commiters for https://github.com/openETCS/model-evaluation repository?

They need to contribute content for the model evaluation task.

Thanks in advance for your help,

Very kind regards

Stan

I added some issues to the wikipage:

https://github.com/openETCS/model-evaluation/wiki/Open-Question-for-Modeling-Benchmark

are my observations correct ?

kind regards

Benjamin

Dear all,

as my last question mentioned a possible spec issue, my question here is, how to handle such things. How should be the process to get information from domain specialists?

I know this is only a evaluation benchmark, but also at this point its annoying to have wrong behavior of the models.

Robustness (D2.6-02-078)

1 unjustified. The tool has been in use to model 44% of subset-026. It is fully functional. No repeated crashes are reported as of today.

Could you please update your quotation?

Documentation management (D2.6-02-078.02)

1 unjustified. Could you please provide a justification, or otherwise upgrade your quotation?

There is the following note:

"The current model does not cover the § 3.5 on session management and the
§4, thus it is di cult to evaluate the capabilities of the language to treat time-outs and
truth tables."

This statement is incorrect, as a good deal of §3.5 is implemented, including timeouts (see for instance this screenshot for timeouts).

Also, the high-priority elements that should be modelled to prove the support of truth tables (HIGH PRIORITY §4.6.2 (Transitions Table) and §4.6.3 (Transitions Condition table)) have been 100% and successfully modelled.

Therefore, could you please:

• remove the note
• mark truth tables and timeouts as supported

test generation score of 0 is inconsistent with test generation score of 2 in section C.8.

Could you please update your score?

This question was raised in munich workshop.

https://github.com/openETCS/model-evaluation/blob/master/Munich_20130416_minutes/Minute%2020130416%20WP7%20evaluation%20matrix.pdf

Dear all,

Could you please vote for my colleague https://github.com/Svitlana-Lukicheva,
to be elected as commiters for https://github.com/openETCS/model-evaluation repository?

They need to contribute content for the model evaluation task.

Thanks in advance for your help,

Very kind regards

Stan

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?

in the following note:

"The current elements (document, GUI) do not allow to give a clear view of the structure and if this structure can be easily translated to the structure of an another language"

Complete translatability to SCADE has been validated as easely automatable by Esterel technologies (confirmed by Esterel during the munich workshop). Therefore, a 1 is unacceptable for "Extensible to strictly formal model" , "Easy to refine towards strictly formal model" and "Extensible to software architecture and design"

Could you please provide better notes for the three above mentioned elements, or provide a compelling justification?

Some Presentations from the Munich meeting are missing!

Distributed software development (D2.6-02-078.03)

the current version of the tool has now splitted the single model and test XML file into one file per namespace, and one file per test, allowing git-based multi-user modelling in a scalable way.

Could you please:

1/ upgrade your note for:

• Simultaneous multi-users (D2.6-02-078.04)
• Version management (D2.6-02-078.07)
• Concurrent version development (D2.6-02-078.08)
• Model-based version control (D2.6-02-078.09) (Moreover, there is now model-based version control implemented in ERTMSFormalSpecs eclipse-based toolchain, on top of EMFStore).

2/ remove the note "The current version of the tool does not allow to define how to have a multi-users development of large scale system."?

Hello,

Do you agree to give committer right to Thomas Bardot on model-evaluation repository?

He works with me on making such models.

Best regards,
David Mentré

Bibliography is missing from Event B model documentation.