Review of D4.2.1 (Systerel)

[MariellePetitDoche]

Introduction

• "This was be accomplished by applying the methods chosen in WP4 Task 1 onto the formal model using the tool chain developed in WP7." I do not think the works presented here have been done based on the toolchain.
• Introduction is very short, and do not present the goal and the contents of the document.
• in the same way, no conclusion or follow-up are provided.

§1 : Institut Telcom

• "The following requirements for the train system are considered in the deliverable." No, only in this section.
• "R3. “The input parameter SD represents the safety distance between two trains and is a constant in the model." Considering SD as a constant is a strong hypothesis really far to concrete case studies. -"There are many formal models related to ETCS [? ? ? ? ? ]." Reference are missing. Why to define a new model then ?
• there is no reference and only a small description of the specification language, is it "IF" as given as example in figure 3 ? -"In this project, we try to use SysML for model specifications. The SysML models are then validated by using SPIN model checker after translating them automatically into Promela." How ? give at least a reference
• How interact tools on, XML, Spin, and the language SysML, IF, Promela is not clear. -§1.4.1, are they properties or Use cases ? Properties are general, here we have some kind of test scenario.
• §1.5, on which model is used the Spin MC ? the one which allow to derive a SIL4 code or the one which allow to generate test ? What is the purpose of this model-checking step ?

Review of the next sections follows.

[MariellePetitDoche]

§2 : TWT

• I have understood the CPN model is build by hand, in parallel to SysML/Scade models. Is it correct ? Can you give a clear view of the input artifacts to define the CPN model ?
• Same thing with the output of the model checking activities , how it can be used to test Scade or SysML model ? Which element is validated : SysML model, Scade, C generated ? Do we have the same level of abstraction.
• § Correctness by Design: besides the refinement question, an important question is which model is validaded ? If it is the CPN model, it is not the one used to design the SIL4 sw, how to interact between this CPN model and the SysML/Scade models ? Are they sufficiently abstract to be simulated ?

[MariellePetitDoche]

§ 3 : Bremen Approach well described, few comments:

• Numbering of sections to correct
• § Method/approach and fig 8 : why you do not start from the same SysML model ?
• "SCADE is EN 50128 certified at SIL 3/4, RT-tester is also certifiable SIL3 as shown in [29]" Tools are qualified not certifiable. level for tool are T1, T2, T3.
• "The next step: 1. Refined test model" How do you plan to proceed ? -"Moreover some missing information in the specification leads to a under constraints test model. It affects the test generation by providing some non realistic test cases." How do you define and manage the added constraints ?

[MariellePetitDoche]

§4 University of Rostock

• § Available specification : give meaning of "TI" and "DMI" ; "form" --> "from"
• Could you explain why you produce 3 different C codes with C different approaches (SystemC, sysMl + Acceleo, Scade ) ? What is the added value to produce these different models ? (especially as SysML seems not adapted for modelling braking curves).
• "On the other hand we use the existing SystemC model to check against a reference model" Thus what is the goal of the SystemC model ? to produce the final SIL4 sw or to produce tests ?
• "Reference model delivered by ERTMS Formal Specs." how do you justify it is a reference model ?
• "Testdata and testcases are provided by ERTMS Formal Specs using the ERA excel data sheet." How do you build the test cases from this elements ?

[MariellePetitDoche]

§ 5 not reviewed, correction made directly.

Review linked to issue #151.

[srieger]

Thanks for the review of our section, Marielle. Here our answers to your comments:

I have understood the CPN model is build by hand, in parallel to SysML/Scade models. Is it correct ? Yes.

Can you give a clear view of the input artifacts to define the CPN model ? The input is Subset 26-5. We will add this information in the report.

Same thing with the output of the model checking activities , how it can be used to test Scade or SysML model ? We have to translate the "runs" of the Scade model to more abstract runs in the Petri net. Thus we will be able to identify flaws in the Scade model in an early stage. In addition, we are working with @janWelte on generating test cases from the CPN model. The SysML model will not contain any behaviour as far as we know; thus, it can be used only to check interfaces and data types. We will elaborate on this in the report.

Which element is validated : SysML model, Scade, C generated ? The Scade model and therefore the generated C code (as the two are equivalent if the Scade code generator is correct which is certified).

Do we have the same level of abstraction? No, the CPN model is more abstract.

Correctness by Design: besides the refinement question, an important question is which model is validaded ? The Scade model (including potentially generated C code) and the specification documents.

If it is the CPN model, it is not the one used to design the SIL4 sw, how to interact between this CPN model and the SysML/Scade models ? Are they sufficiently abstract to be simulated ? We do not understand this question. Could you please clarify?

[nhnghia]

Dear Marielle, Thank you for reviewing the section of Institut Mines-Telecom. We have taken into account your comments in our new version. Here are some answers to your questions.

"R3. “The input parameter SD represents the safety distance between two trains and is a constant in the model." Considering SD as a constant is a strong hypothesis really far to concrete case studies.

This is to seek simplicity at the first period. It will be refined in the next time.

there is no reference and only a small description of the specification language, is it "IF" as given as example in figure 3 ?

We are trying submit our UserStories on the GitHub

"In this project, we try to use SysML for model specifications. The SysML models are then validated by using SPIN model checker after translating them automatically into Promela." How ? give at least a reference How interact tools on, XML, Spin, and the language SysML, IF, Promela is not clear. §1.5, on which model is used the Spin MC ? the one which allow to derive a SIL4 code or the one which allow to generate test ? What is the purpose of this model-checking step ?

We are going to use IFx as model-checker for IF specifications instead of the Spin for the Promela specification. We are also studying the transformation from SysML model to IF model. This has been clarified in the last version of our section. The model-checking step is used to verify a ETCS model against some properties, i.e., when a model satisfies a property, its implementation satisfies also the property. Our current model will be refined to take into account different function modes of OBU as described in Subset-026.4

§1.4.1, are they properties or Use cases ? Properties are general, here we have some kind of test scenario.

I think we could call them as properties in the point of view of model-checking, i.e., model satisfies some properties, but also as user cases in the point of view of testing, i.e., SUT passes some test use cases.

[alexn84]

Dear Marielle, great thanks to you for reviewing the section of the University of Rostock.

Could you explain why you produce 3 different C codes with C different approaches (SystemC, sysMl + Acceleo, Scade ) ? What is the added value to produce these different models ? (especially as SysML seems not adapted for modelling braking curves).

Well, as an University we want to see what methodologies are possible and practical, so perhaps this seems to be some kind of to academic to you. We want to compare different approaches and this works only if you have the same base. So we defined a subset of the spec from where we think we could model it in different languages and usage of different tools. The purpose is: hw/sw co-design If you want to develop an onboard unit (hw/sw design) you need to know e.g. what kind of processor/memory/scheduler is necessary to calculate safety critical stuff in time. On the other hand, you cant develop satisfying software without knowing the target platform. To ease the decision what hardware will be sufficient to meet the requirements you have to estimate the current and future software effort (very long life cycle of the OBU). With our approaches we can predicate in very early stages of the system development which hardware will be needed because we can simulate the behavior of the system with virtual prototypes. Additionally we produce different abstract models for WP3 and we contribute to the verification activities. So there is an added value in my eyes.

As you say: We don't know yet whether SysML is good for modeling braking curves, so we want to have evidence regarding this statement.

"On the other hand we use the existing SystemC model to check against a reference model" Thus what is the goal of the SystemC model ? to produce the final SIL4 sw or to produce tests ?

SystemC will be used for simulation and testing. E.g. performance estimation as already mentioned, so called: testing extra-functional aspects...

"Reference model delivered by ERTMS Formal Specs." how do you justify it is a reference model ?

We can't. But for now there are no other models available. Perhaps "reference" is the wrong word ;-)

"Testdata and testcases are provided by ERTMS Formal Specs using the ERA excel data sheet." How do you build the test cases from this elements ?

By hand, but this will be discussed in future WP4-Sessions. We are working on a common format and automation.

[MariellePetitDoche]

@srieger : thanks for your answers.

"Correctness by Design: besides the refinement question, an important question is which model is validaded ? The Scade model (including potentially generated C code) and the specification documents.

If it is the CPN model, it is not the one used to design the SIL4 sw, how to interact between this CPN model and the SysML/Scade models ? Are they sufficiently abstract to be simulated ? We do not understand this question. Could you please clarify?"

My question seems now out of the scope. I understand that the CPN model is an abstract model which allows test case generation to validate the Scade model. Then the main challenge of a correct-by-construction design is now to identify the step and interactions between Scade and CPN models.

[MariellePetitDoche]

@nhnghia and @alexn84 : thanks for your comments.

[MarcBehrens]

Review closing session 19.3.2014:

• [x] Comment on review for section 3 pending @cecilebraun
• [ ] For a last (new) section a conclusion on the approaches of the partners is missing. @jfrsantos
• [ ] Next steps foreseen in the task as outlook on the next deliverable are missing linking the approaches.@jfrsantos .

[cecilebraun]

Dear @MariellePetitDoche thanks for the review and sorry for the delay

  § Method/approach and fig 8 : why you do not start from the same SysML model ?

We want to verify the SCADE model and not the fact that the generator are correct.

[MarcBehrens]

Review closing session 02.4.2014: Issue pending @nhnghia

[MarcBehrens]

New version committed ec53ff3e74fd291286f2c668b66b79fac2b83c93 @MariellePetitDoche is there still something missing?

[MariellePetitDoche]

Contents of this issue were mainly questions to have a better understanding of the approaches. Answers done are fine for me. I close the issue.