D7.1 Toolchain Schema Proposal

[MatthieuPERIN]

The CEA, as the main holder of SysML Model, have worked with some partners on the 28th of august at Paris in order to propose a representation of what could be the data processing from inputs (SRS, EFS contents, SSRS, Rail knowledge,...) to outputs (Code, safety analysis, ...) trough the several WorkPackage (WP3, WP4, WP5, WP7) that will rely on the semi formal SysML model.

This proposal may be found here : https://github.com/openETCS/toolchain/tree/master/PositionPapers/CEA/2013_08_28_D7.1_Toolchain_schema_proposal

We invite all partners that will use the semi-formal model (almost everyone as far as we know) to have a look at the proposal and to give a counter proposal if they do not agree at some point. We think that this schema may be helpfully added to the D7.1 document to clarify the whole data processing.

Please give feedback within a week !

[cponsard]

the figure looks great and would definitely be helpful in D7.1 and more generally to help have a good vision of the links across WPs.

It need some complementary explanation. e.g. I see the point with WP3 and WP7 but I am less familiar with WP4 part:

• what is internal assessment, is it related with tool chain qualification as other link with WP7 + add some arrow there I guess
• validation could point to prose/early model while verification intermodel/code (but this could overload the picture)

on the top level, we could also position also the ERTMS subsets & API

[stanpinteTheSignallingCompany]

Dear Mathieu,

Some comments/questions:

1/ why do you put ERTMSFormalSpecs in WP7, and SCADE in WP3? Currently, there is no decision on how to proceed (see latest WP3/WP7 issues). It is totally possible that both ERTMSFormalSpecs and SCADE are used for WP3 (and maybe even more solutions, like SysML, why not?)

2/ My understanding of the picture is that CEA intends to model the semi-formal model (which should cover 100% of Subset-026) in SysML only. I have two main concerns regarding this proposal:

2.1/ I Are you sure you can represent 100% of Subset-026 in an understandable, executable, testeable way in SysML?

2.2/ Do you think there are enough resources in WP3 that are ready to invest in a 100% SysML model? If not, then the approach might not be feasible.

3/ This figure should be in line with following figure (See https://github.com/openETCS/SSRS/blob/master/Workshop%202013-03-28-Charleroi/MoM%20SSRS.pdf):

That figure has been discussed a lot, and seems to reach consensus, and we should avoid summarizing it again, and loose some very important differences (for instance WP5 demonstrator doesn't take as input SIL4 code, but SIL-nothing code.)

Very kind regards

Stan

[KlausRuedigerHase]

Dear Matthieu,

I would like to complete the drawing with some some details respecting the EFS modeling, which should be continued in parallel to the SCADE modeling, allowing us to compare results on model as well a executable code level (given that the "EFS to C Code" has been developed, what Stan expects to be done in 6 MM). While ESF does not claim to develop SIL 4 code, SCADE is suppose to do so, as well as that the SCADE code generator can generate optimized compact code for embedded control systems certified according to CENELEC EN50128. Stan, we definitely will not have sufficient resources to do more than the models in 2 alternative groups, that should be EFS (for a semi-model with the EFS domain specific language, down to C code non-SIL grade for non vital executable code) and SCADE (Lystre) Model (for a model that can be either used for non-SIL code with semi-formal or SIL4 code with semi- as well as strictly formal model, generating code with that certified code generator). That figure 1 above may have been discussed a lot, but mistakenly identifies SIL4 with formal and non-SIL with semi-formal, for which there is no justification in CENELEC. In addition we want to have "SIL4 quality code" to be generated for our reference OBU hardware, which means is has to be proven to be "functionally correct" (proof of function, not safety is needed), but not necessarily been implemented in a SIL4 hardware. That hardware can be a non-SIL hardware, no need to be fail-safe, but the software need to be of highest level of correctness. Therefore applying formal methods might be very helpful to proof functional correctness according the formal specification. .

Therefore I would like to change Matthieu's picture:

1.) Left part represents only WP7 tools development activity (no modeling until tools are ready to use, down to C Code). The goal for WP7 is to find a migration path from the closed source SCADE modeling and code generation tools chain to an open source tools that allows to reuse models and other artifacts created with SCADE in an open source domain. Since POLARSYS has a similar tools chain in its focus, cooperation is highly recommended.

2.) SCADE tools chain is the one we are using for SIL4 quality formalization, modeling and C code generation for the reference OBU. Today SCADE is the only CENELEC certifiable tools chain to generate a SIL4 grade formal specification/model as well as SIL4 code.

3.) EFS tools chain is the only OSS tools chain for creating semi-formal specification and model, based on a domain specific language AND a substantial part of the SRS has already been formalized and therefore we want to complete this work. Expecting a C-Code generator from EFS will also provide non-SIL C code, useful for rapid prototyping. We can and should use the EFS semi-formal model as well as EFS generated C code for verification with SCADE artifacts: Comparing the model as well as the executable code. That allows us a direct comparison between two different modeling tools and code generation mechanism. In addition the EFS content already available should be used to feed the "System Analysis" and "SysML Semi-Formal Model" in the top two bubbles.

4.) WP4 V&V activities, utilizing different methods and tools. By providing a 2nd model description and 2nd executable C code from 3.) , the EFS artifacts can therefore become also V&V tools for SCADE artifacts.

5.) WP5 Simulation will then feed the demonstrator with C code coming either from the EFS tools (non-SIL rapid prototyping code), SCADE tools (non-SIL or SIL4 grade software for OBU reference purposes) in the short term. In the long term, once the alternative OSS tools chain is available that SIL4 grade executable software will be made available from the OSS tools chain.

KRH

[UweSteinkeFromSiemens]

Dear Matthieu, I agree with the additions of KRH to the diagram. Moreover, WP4 (V&V) will not only be fed by the semiformal model; V&V could address the "Code Model" level as well as the generated code (C, ADA, ..) level as verification objects. For clarity, the diagram should be enhanced with such arrows or links.

[MatthieuPERIN]

Dear Klaus and Uwe, I have taken into account your suggestions, the documents have been updated:

Dear Stan, some answer have been done by Klaus but I will add my own:

1/ why do you put ERTMSFormalSpecs in WP7, and SCADE in WP3?

SysML, as the Semi-formal model reference, will mandatory be used in WP3 at least as the starting point for toolchain and more is partner need to (using some profile to format data for tool for example). The proposition made by Klaus may answer as well, using some EFS artifact to perform V&V on SCADE. Such artifact may be integrated into the SysML model if needed.

2/ My understanding of the picture is that CEA intends to model the semi-formal model (which should cover 100% of Subset-026) in SysML only. I have two main concerns regarding this proposal:

No, the CEA will support the Meta-model (model of the model) and will help modeling the subset 26 and all other source but will no support all the modeling.

2.1/ I Are you sure you can represent 100% of Subset-026 in an understandable, executable, testeable way in SysML?

Understandable way, yes, with no doubt after the workshop we have at Massy, testeable also. For the executable way I will ask you some precision, as a large part of the subset 26 is not at code-level specification, the execution of such requirements is to me an open question.

2.2/ Do you think there are enough resources in WP3 that are ready to invest in a 100% SysML model? If not, then the approach might not be feasible.

Why invest in 100% in SysML ? I will be glad to work with you to improve your ecore model of data in order to enrich the SysML model with the 44% already done in EFS (as you may have notice, EFS content is precised as a source to the SysML model), for the remain 56% if the partner prefers to use EFS to model the subset 26 it is fine to me.

3/ This figure should be in line with following figure.

I do not see major differences as the SysML model is to be the SSRS semi formal model, it will include Req from subset 26, results from V&V if needed and will be the starting point for formal code model for SIL4 and non SIL4 code generation as presented in the Figure you gave. It is just that this proposal is a more precise and concrete representation of the tool chain to me.

For my part I am not convince by the Figure B1 on the D7.1 as the Papyrus branch seems to be a dead end. To me the SysML model is central as it is open and not related to a tool, letting everyone use it and enrich it at pleasure (safety, V&V, ...).

[stanpinteTheSignallingCompany]

@MatthieuPERIN

Some precisions regarding executability: the Subset-026, expressed in ERTMSFormalSpecs, is completely executable. We think executability is a very important feature. It ensures non-ambiguous behavior, which in turns ensures the possibilty to generate source code from the model.

[UweSteinkeFromSiemens]

Now, the actual diagram version is ok for me.

[MatthieuPERIN]

@stanpinte

Dear Stan,

Thanks for your answer but please answer my question, I m not asking what ERTMSFormalSpecs do, but:

• What is your definition of executability for a non-code level requirement in subset 26. For example how do you "execute" Req 5.18.9.1 "This procedure is dealing with the indication to the driver of a request to sound the horn." ?
• As you talk about behavior, what is the formalism and semantics use for behavior modeling in EFS, please precise me:
  • How do you manage concurrent evolution ?
  • Have you synchronous or asynchronous evolution ?
  • Do you manage timed behavior and/or temporal behavior ?
  • Do you manage continuous behavior ? In a decidable way ?

For sure you are right about the fact that executability is a very important feature because it ensures non-ambiguous behavior, which in turns ensures the possibility to generate source code from the model.

This is why generally designer tend to use formal tools to design and are not relying on semi-formal models only which behavior may be ambiguous.

Kind regards,

Matthieu

[stanpinteTheSignallingCompany]

@MatthieuPERIN

I'll ask one of our ERTMSFormalSpecs specialist to get back to you asap (in the coming hours, don't be afraid :))

Indeed, executability matters, and we at ERTMS Solutions are ready to provide a warranty of non-ambiguity and executability of ERTMSFormalSpecs model.

SCADE also does.

I look forward to any commercial company doing the same with 100% SysML model.

[Svitlana-Lukicheva]

@MatthieuPERIN

Dear Matthieu,

Please find my answers below.

• What is your definition of executability for a non-code level requirement in subset 26. For example how do you "execute" Req 5.18.9.1 "This procedure is dealing with the indication to the driver of a request to sound the horn." ?

  Obviously, a set of paragraphs of Subset-026 cannot be executed, since it contains titles, definitions, notes, deleted requirements…. In ERTMSFormalSpecs, each paragraph is verified and is marked as requirements if it has to be implemented/executed, or as title/note/deleted in other cases. The paragraph you mentioned will be marked as “Definition” in EFS. Here, we are talking about the executable part of the Subset-026.

• As you talk about behavior, what is the formalism and semantics use for behavior modeling in EFS, please precise me:

  • How do you manage concurrent evolution ?

  The EFS system state is represented by a set of variables. While implementing the model, our engineers have to respect the fact that one variable cannot be modified more than once during one execution cycle (and one of the next features to implement will be a check verifying that this constraint is always satisfied). Obviously, sometimes one variable may change several times during the cycle execution (suppose you receive some information in a balise group, you store this information in the internal variables, but for example after a mode change, you have to delete it according to the table in Chapter 4.10). To handle this problem, we sub-divided the execution cycle in several sub-cycles (see §4.8 of the User Guide), allowing to handle these two updates separately. In the case when the priorities for a variable update are explicitly assigned by the Specification (for example, in the Transition Table 4.6.2), we implement this update in one sub-cycle, using “if-else” like expressions.

  • Have you synchronous or asynchronous evolution ?

  Could you please precise what exactly do you mean by synchronous or asynchronous evolution?

  • Do you manage timed behavior and/or temporal behavior ?

  Yes, we have a variable representing the current time, and a set of timers. Our test environment allows testing properties on these timers. It also allows going back while executing a test, in order to verify the state of the system at previous cycle.

  • Do you manage continuous behavior ? In a decidable way ?

  No, our variable representing the current time of the system is updated once per cycle, by a configurable cycle time increment. This is in line with what happens in a real EVC.

[KlausRuedigerHase]

@MatthieuPERIN: Thanks for the addition, I perfectly agree with it. @StanPINTE: I assume from your comments that you can agree with this approach as well. I personally believe that this gives you a perfect opportunity to demonstrate that EFS can compete with modeling capabilities of similar tools and by that we have a perfect way to compare an open tool with an closed source tool that is well accepted in the.industry., which I hope will improve acceptability OSS in general. Thanks KRH

[stanpinteTheSignallingCompany]

@KlausRuedigerHase Dear Klaus, I agree indeed, if you could retitle the ERTMSFormalSpecs column in the picture, from "EFS modelling for SCADE V&V " to "WP3 EFS-based modelling".

Do you think such small change would be acceptable? With this change, ERTMSFormalSpecs model can in all cases be used for V&Ving the other (SCADE for instance) model, but at least it locates ERTMSFormalSpecs modelling in WP3 (where most of our resources are, we don't have any in WP4).

If acceptable, then I would agree with it.

[KlausRuedigerHase]

Dear Stan, I would not put too much effort in "titles". I personally do not have any problems to put whatever it takes into EFS modeling, independently from the question of WP allocation. "WP3 EFS based modeling" would be fine for me as well. As long as we are making progress, it really does not matter. KRH

[MatthieuPERIN]

@Svitlana-Lukicheva

Dear Svitlana, thanks a lot for the precision !

• Considering the "executability" of 100% of subset 26: For Sure I agree with you on the fact that not all the subset 26 "requirements" are behavior related (definitions, title, ...) and thus cannot be executed. For the executable requirements -generally text with flowcharts or conditional sentences- the solution in SysML is to use either state machine (fir mode change for example), activity diagrams (for flowcharts) or sequence diagram when needed (suits very well scenario-like requirement)
• Considering the behavior used within EFS, I understand well your cycle-base semantic (based on sub cycle and eventually using the priority given in the subset 26) but I have still some minor questions:
  • How do you manage case where the subset 26 do no give priority on evolution, for example given two flowcharts that may have to evolve simultaneously without a precision given over their respective priority, do you make them evolve simultaneously (synchronous behavior), do you force an order (asynchronous behavior) or do you let the possibility to have all the previously cited behavior (asynchronous non-deterministic behavior with synchronization capability).
  • You use a variable to model time, is the evolution of this variable is forced by a constrains system base on timed constrains or let free to "force" the model to evolve without being in a deadlock. Do you allow interval in timed constrains and how do you model "instantaneous" or non-timed evolution ? Do you use priority semantics ?
  • For the continuous behavior you have to model quite well the hardware also in order to have variable refresh time cycle close to a real implementation, how do you manage to do so ?

Thanks a lot again for your precision, I have a clearer understanding on the EFS model now, I hope you will answer my new set of questions, asked because I am very curious and interested by your first answers !

[astante]

I think this image captures quite well the current discussion regarding the different tool chains. I have some questions and thoughts regarding the feasability.

1. Probably it is not already defined an open. But, I'am interested into what diagrams are expected to be used in the SysML modeling? The questions arises from the practical standpoint that the diagrams have to be transformed for example into B. I think it is quite for sure is that BBD and IBD will be used. But how about behavior? Probably this question is out of scope in this discussion here. All of this influcences the availability of the toolchains.
2. Although the OSS migration path is often mentioned, I have some doubts going from SCADE to B. Probably @MariellePetitDoche and @MERCEmentre are more qualified regarding this question and share or disagree my concerns. SCADE and B are different methodologies. I think it will be very difficult to create a transformation from SCADE to B which preserves all the semantics. It is not a matter of file format description or description of the language. It is the matter of mapping the semantics of both languages. I personally see the only migration path from SCADE to B at the SysML level. The SysML model in Scade System (which is also modelled with Papyrus) could be used in the B toolchain. As far as I know it only contains structural information.

[MariellePetitDoche]

Dear Alexander,

1. This is a topic which shall be covered by D2.4. Please to follow this issue: https://github.com/openETCS/requirements/issues/19 , contributions are welcome.
2. I totally agree with you and it is what I said during yesterday telco (but we can extend the comment too lots of formal approaches). Other kind of migration to investigate is on some subpart of description as state-machine, data flow,... For lower levels I think that the gap between Scade and B approaches (our others) is too large to imagine an easy migration.

[MERCEmentre]

I agree with both Marielle and Alexander that it would be difficult to go from SCADE to B.

[cyrilcornu]

By all4tec side, we agree on this scheme, even if some questions still remain:

• Is the SysML Model supposed to be considered as Input for Design phasis for each proposed tool (Scade, OSS, EFS)? If so, shouldn't we focus now our efforts on it?
• Is the OSS toolchain meant for support B or EFS, or other? This point remains unclear for us in the current version of the Scheme.
• Validation on Scade model with EFS help could be an interesting approach, but have we already some technical perspectives on what can be done?
• It is unclear for me, whether Scade Suite or Scade System is considered when talking about Scade. As a reminder, a Scade System model is 100% SysML model. The import from Scade System models into Scade suite is automated, but only the system architecture is imported. The behaviour has then to be build in the Scade Suite model. So shouldn't we present these Scade modeling steps in the scheme, as the architectural aspect is to be considered at the SysML Model level. @UweSteinkeFromSiemens , could you please aknowledge or correct me on this point?

[UweSteinkeFromSiemens]

Dear Cyril, you 're correct. The actual version of SCADE System allows to model a systems functional structure and its architecture on SysML. The capability of behavioral modeling with automatic transfer to SCADE Suite is under development, but not available right now. In sum, we could start to set up the functional and structural system structure wie SCADE System and automatic transfer to SCADE Suite, and then enrich the SYS/ML model with behavioural models like state machines or action diagrams. These behavioral models could be used for manual or automatic export (as far as transformators exist) to B or EFS. The export of behaviors to SCADE Suite must be done manually now; as soon as behavioral modelling is available in SCADE system, the manual export could be replaced by the automatic synchronization between SCADE System and SCADE Suite.

I'm actually working on a SCADE System model on top of the existing MoRC (management of radio communication) model to show how such a combination of functional and structural system structure modelling with SysML and fomal modelling with SCADE Suite works. I will put it on github soon.

[cyrilcornu]

Dear Uwe, Thank you for your precisions on Scade! Great that you will provide a Scade System model, it will help a lot!

[jastram]

This has been incorporated with 0296440b4c8e61b6c6dcde2777415d34199a94d7

[MatthieuPERIN]

Re-open because I am still waiting for answers from @stanpinte or @Svitlana-Lukicheva over some semantic precision on EFS.

And proposition made by @jastram in #150 has to be discussed:

There is a flow from primary sources over prose analysis (the former SSRS) to SysML, however also a direct link is drawn from primary sources to SysML.

I don’t agree on the direct link because it will lead to traceability issues.

Of course in the prose, references can be made to primary sources which than can be used as input for SysML, but I oppose the direct link.

[JanWelvaarts]

I have some problems with the flow between the input documents and SysML. In my opinion the model should be based on the functional structure (system analysis) to be described in "prose", otherwise proving traceability will be difficult.

[stanpinteTheSignallingCompany]

@MatthieuPERIN I opened an issue in ERTMSFormalSpecs repository, related to your semantics questions.

https://github.com/openETCS/ERTMSFormalSpecs/issues/128

These questions would be best answered by our ERTMSFormalSpecs language and toolchain specialist, @LaurentFerier.

I'm sure similar questions can exist on other toolchains, so I would like this issue to be non-blocking for the ongoing D2.1 review.

Is this allright with you if @LaurentFerier handles all your questions next week?

[MatthieuPERIN]

Dear @stanpinte,

You did right !, do not press your colleague because I will be on vacation next 2 weeks.

I have modified the column name for EFS, please have a look !

Dear @JanWelvaarts, I do not see where the issue is really present, but, as the asked modification have not been contested by partner, I have made it.

New version of the proposal is below:

As it will probably be integrated into D7.1 Conclusion, I ask again to any partner that disagree on this schema to step in and propose an argued/expressed modification.

[stanpinteTheSignallingCompany]

@MatthieuPerin thanks !

  From: Matthieu PERIN [mailto:notifications@github.com] Sent: mercredi 11 septembre 2013 14:15 To: openETCS/toolchain Cc: Stanislas Pinte Subject: Re: [toolchain] D7.1 Toolchain Schema Proposal (#144)

  Dear @stanpint,

You did right !, do not press your colleague because I will be on vacation next 2 weeks.

Dear @JanWelvaarts I do not see where the issue is really present, but, as the asked modification have not been contested by partner, I have made it.

New version of the proposal is below:

As it will probably be integrated into D7.1 Conclusion, I ask again to any partner that disagree on this schema to step in and propose an argued/expressed modification.

— Reply to this email directly or view it on GitHub.

[cponsard]

note there is a problem in the figure reference in D7.1 just below the figure in decision 5

[MariellePetitDoche]

Reference corrected and legend of fig5 cleaned : No decision have been made concerning EFS part of WP3 or not according: https://github.com/openETCS/model-evaluation/wiki/D7.1-review

in version 01.01

[MariellePetitDoche]

in https://github.com/openETCS/toolchain/commit/8c0d54ec53d3e2d5f014949676333c8a4d98f914

[MatthieuPERIN]

EFS semantic issues transferred in issue https://github.com/openETCS/ERTMSFormalSpecs/issues/128

Figure corrected and accepted by partners (review meeting of the 9th and 12th of September).

Source and Image moved to D7.1\image (as requested in issue #151 ) and old directory renamed with "_backup" and keep only for memory purpose.