openETCS / requirements

WP2: Top Level Project for openETCS requirements
5 stars 13 forks source link

Is a SSRS needed between SRS and model? #8

Closed sbaro closed 11 years ago

sbaro commented 11 years ago

We had a discussion (SNCF + Cyril Cornu) regarding the need of a document between the SRS and the formal model.

The SRS SUBSET-026 is a system specification:

The first purpose of this document will be to distinguish the onboard requirement from the trackside requirement.

The second purpose will be to provide the functional architecture of the OBU and OBU kernel. It will clarify which part of the OBU will be in the model, and what will be the interface with the outer world. It will also provide the internal functional architecture of the model (Safe Braking Model, Localization, Mode management,...) and the interfaces between each functions. Eventually, it will provide an allocation of the requirement into the functions, and the tagging Safety/Non Safety of the requirements.

The requirements will need to be modified for two reasons: they will need to make use of the I/O identified in the functional architecture, and they will possibly need to be cut down in order to fit into the functions (some SRS requirement could possibly correspond to two SSRS subrequirements allocated to two functions).

Downstream this document, we think that there is no need for a SwRS. The model should be defined at the highest level possible, and the purpose is that the software part will be refined (or generated in some way) from the formal model. It is however clear that introducing a SSRS will lower slightly the level of the formal model: it is not a straight from the SRS to the model approach.

The pros:

The cons:

mgudemann commented 11 years ago

In my opinion, this is a good idea. Of course, I am aware of the "cons", but the requirements of the SRS could well be traced in the proposed SSRS. For example, if some SRS requirements will be split into two or more functions and requirements of the SSRS, this can well be documented (e.g., with tools like ProR). It should still be possible to verify the original SRS properties in a more structured formal model.

Particular in the light of the planned code generation, a more structured model is desirable, CENELEC is quite clear in the requirement to have a defined SW architecture.

I think that having a more structured model wrt. architecture and safety / non-safety relevant functions would be an advantage. The proposed SSRS should be well suited to support this.

MariellePetitDoche commented 11 years ago

I am fully agree that a work is necessary on the SRS to highlight the internal structure of the functions, elicite global variables and data flow between functions, allocate requirement, and so on. I am agree with all your pros. For me, this shall be done in WP3 Task1.

However, for your cons, I think we can find semi-formal or formal means better than raw informal description : for example SysML is dedicaded to challenge such kind of problematics, or some studies on requirements management are done around the ReqIF standard and formal methods (for example Kaos, ProR which is link to eventB,... ). It is plan in WP7, task 2 to identify supporting tools and methods to capture and mange requirements.

MERCEmentre commented 11 years ago

Like Matthias and Marielle, I agree that work on SRS is needed to extract its internal structure, for all the good reasons you mentioned.

Like Marielle, I would prefer using a semi-formal approach (SysML comes to mind) embodied in a computerized model, for several reasons:

On the other side, using a certain formalism (like SysML) might restrict the ability to describe clearly the SRS content (ability to make dedicated graphics, etc.), so a paper approach might be more efficient and clear in practice.

sbaro commented 11 years ago

What I had in mind was more like paper and natural language. Indeed, going down from system to subsystem is a step, and providing some internal architecture is another step. I think both these step could be combined in one (SRS -> SSRS) because they all deal with refining the requirement, chosing who is "in" and "out".

But (IMHO), introducing some formal language is another step (a big one), and I am not sure that it is a good idea to formalize in the same move than the refinement. I am not an expert in formalizing, but I feel that it mixes two different conceptual steps. In other word, I think that the proper path is the one when there is the smallest gap (in terms of level of abstraction) during the formalization step.

Pres

stanpinteTheSignallingCompany commented 11 years ago

Dear Sylvain,

Thanks for this clear email.

I agree with your points, that the Subset-026/SRS mixes OBU and TRACK requirements, architecture clarification and safety classification of requirements.

However, the "cons" you list

The cons:

introduce another level of natural language between SRS and model (... which may allow to introduce interpretation and errors) 

in my opinion shall far outweigh the benefits of adding an extra layer of indirection between the SRS and the model.

I think that if we use the following structure:

SRS <--> SSRS <--> model, then we shall lose a critical aspect: the easy verification of model versus SRS. That aspect is totally critical for the following stakeholders of the project:

I would rather suggest the following approach:

From these points, ERTMSFormalSpecs already does from 1/ up to 4/ already.

--> Actually, the model becomes sort of an SSRS, but formalized, executable, verifiable, testeable, and with full traceability towards SRS/S026.

That way, you can have the pros, without the cons, but inside a formal model. Of course, at some level your model shall require model documentation, explaining how it is structured, its grammar and semantics, etc, but that way you avoid having an SSRS introduce another level of natural language between SRS and model.

Very kind regards

Stan

stanpinteTheSignallingCompany commented 11 years ago

Dear all,

To sumarize on that very interesting discussion:

1/ I agree with @MERCEmentre and @MariellePetitDoche about the need of a formalized SSRS (in my opinion it is more a model enriched so that, following Marielle wording "[it can] highlight the internal structure of the functions, elicite global variables and data flow between functions, allocate requirement, and so on..."

2/ I agree with @MariellePetitDoche that that task should occur in WP3 Task1. --> Should be added to the WP3 DoW...another thing to do urgently :)

3/ @MERCEmentre already mentioned in the past the problems you arise when you have several models: how do you ensure they are synchnronized and consistent? Therefore, if we use a high-level language like SysML, how can we make sure it is always synchronized with the actual model? -> to me, we need to have round-trip engineering there...

Questions now:

4/ @sbaro: would it be possible to send me the ppt source of your chart, so that I can reuse for the future WP3 Dow, section T1?

5/ @mgudemann: Mathias, in my opinion we could use different architecture for the model and the generated code. One essential of the model is to be verifiable against Subset-026, and that is not a goal of the generated source code. The generate source code has only to by compliant with CENELEC requirements. If course it needs to be modular, but the kind of modularity you need on generated source codes (typical volume: 500.000 - 2 million LOC I would say) is not the kind of modularity you would need on a Subset-026 formal model (typical volume: between 10.000 and 50.000 model artifacts, versus the +- 3500 applicable Subset-026 requirements). Both modularities have different goals. What do you think?

MariellePetitDoche commented 11 years ago

"1/ I agree with @MERCEmentre and @MariellePetitDoche about the need of a formalized SSRS (in my opinion it is more a model enriched so that, following Marielle wording "[it can] highlight the internal structure of the functions, elicite global variables and data flow between functions, allocate requirement, and so on...""

No if we use formal methods we can benefit of all verification mechanism behind formal methods as quoted by David : it is not just a graphical or organized viewpoint, it opens the possibilities to introduce strong verifiaction on the link and interfaces between functions, consistency and complementarity between them, coverage in regards of requirments,...

MariellePetitDoche commented 11 years ago

"5/ @mgudemann: Mathias, in my opinion we could use different architecture for the model and the generated code. One essential of the model is to be verifiable against Subset-026, and that is not a goal of the generated source code. The generate source code has only to by compliant with CENELEC requirements."

What does mean generated code ? How can its architecture be different from an highler level model if it is generated ? Are differeneces been introduced by the "generator" ? in this case, how we can prove that these introduiced mechanism are compliant with a safety process in regards of CENELEC 50128 ?

stanpinteTheSignallingCompany commented 11 years ago

@MariellePetitDoche

I think we agree. It is not because the model "[it can] highlight the internal structure of the functions, elicite global variables and data flow between functions, allocate requirement, and so on..." that it doesn't allow you to perform strong verification and consistency checks, coverage checks, etc.

stanpinteTheSignallingCompany commented 11 years ago

@MariellePetitDoche

In answer to your question:

What does mean generated code ? How can its architecture be different from an highler level model if it is generated ? Are differeneces been introduced by the "generator" ? in this case, how we can prove that these introduiced mechanism are compliant with a safety process in regards of CENELEC 50128 ?

The actual Subset-026 has to be transformed to one or more intermediate languages, up to the point it becomes executable on hardware (compilation).

For instance, you could imagine the following:

Subset-026 model -> SCADE model -> C code generated with KCG (http://www.esterel-technologies.com/products/scade-suite/do-178b-code-generation).

Nothing prevents the C source code generated by KCG to have very different low-level architecture than your Subset-026 model. But maybe we mean different things by architecture?

This the whole challenge of making a certifiable code generator, by the way: you have to demonstrate that the transformations you apply to the model to reach final source code are compliant with EN50128 requirements for the target SIL level.

MariellePetitDoche commented 11 years ago

@Sylvain,

I am agree we are mixing two concepts :

Thus, in your figure, I think we can slide the SSRS box on the right just on the line between natural and formal.

sbaro commented 11 years ago

@MariellePetitDoche

OK, I agree with you (if I understand your point, because I am not familiar with the tools you mention).

If I rephrase:

Is that it?

The point where I disagree with @stanpinte being that in his opinion, it is better to formalize the requirement as soon as possible.

sbaro commented 11 years ago

Sorry for the unwanted closure... I just hate this tool...

stanpinteTheSignallingCompany commented 11 years ago

@sbaro

No problem for the closure!

Sylvain, I understand your disagreement, but one of the major goals of the project (I refer to the PCA) is to create "(a) Creating a formal specification of the ETCS OBU functionality according to UNISIG Subset 026".

That formal specification must be 1/ understandable by domain specialists and 2/ verifiable against Subset-026.

That's why we think (one of the bases of the ERTMSFormalSpecs approach) that the link between the formal model and the Subset-026 should be straightforward.

You can't touch the Subset-026. At least not in a way that is not immediately understandable by someone from the ERA (a railway specialist), that doesn't know what a model refinement is.

Therefore, I see the use of having an SSRS document, but I think this document should not prevent that goal: to have a model which is just like Subset-026.

During our workshop in Brussels, railway specialists outside the consortium (the ERA, the ERTMS User Group, the SSICF = belgium ministry of transport, division ERTMS) agreed it is possible with ERTMSFormalSpecs.

--> I'm advocating very strongly not to break that very close relationship between Subset-026 and the model.

One doesn't need to break that S026-model intimacy, so important for railway domain experts, in order to achieve the "pros" of the SSRS listed above, in your first email:

The SSRS just need to take that intimacy into account.

Feel free to call me if you wish to discuss more.

MariellePetitDoche commented 11 years ago

@stanislas : " The actual Subset-026 has to be transformed to one or more intermediate languages, up to the point it becomes executable on hardware (compilation). "

Each step of transformation has to be verified, by reviews, by formal proof or by test. Is one of the main advantage of structured formal mathods as classical B at software level to allow tool supported methods of transformation of the maodel, with strong formal proof capability. But the last transformation from the concrete executable B model to a target language (as C or Ada) does not transform the software architecture. It is the same with SCADE and KCG : the software architecture is defined (and verified) on the SCADE model and transformation via KCG has no impact on the architecture.

" For instance, you could imagine the following:

Subset-026 model -> SCADE model -> C code generated with KCG (http://www.esterel-technologies.com/products/scade-suite/do-178b-code-generation).

Nothing prevents the C source code generated by KCG to have very different low-level architecture than your Subset-026 model. But maybe we mean different things by architecture?

" Code generated by KCG will have a very different "software architecture" from the "system architecture" of subset 026. And the transformation from a formal "software architecture" to a generated code (for example with KCG) is not a problem and industrial have a lot of experiences to ensure it. But the main issue is how to manage and verify the transformation from a "system model" as close as possible from the subset 26 with a given system architecture to a "software model" with a software architecture which allow to generate executable for a given target. Currently, in railway industry, this step is done by review between software models and system documentation.

" This the whole challenge of making a certifiable code generator, by the way: you have to demonstrate that the transformations you apply to the model to reach final source code are compliant with EN50128 requirements for the target SIL level. " In my point of view, this point is sufficiently well known by the railway industry and commercial tool suppliers, do not be the more crucial part of a R&D project.

stanpinteTheSignallingCompany commented 11 years ago

@MariellePetitDoche

Thanks for your detailed comment.

But the main issue is how to manage and verify the transformation from a "system model" as close as possible from the subset 26 with a given system architecture to a "software model" with a software architecture which allow to generate executable for a given target. Currently, in railway industry, this step is done by review between software models and system documentation.

This raises interesting questions:

--> The "system model" and "software model" should be the same models, in my opinion. This is the approach we used in ERTMSFormalSpecs.

--> If you introduce a manual translation / manual verification by review step between the "system model" and "software model", then you loose verifiability of the Subset-026 model by domain experts.

MariellePetitDoche commented 11 years ago

@ stanislas : " This raises interesting questions:

Which model do you test functionally?
Whic model undergoes Subset-076 tests?
Which model shall domain experts be able to review against Subset-026?

"

" --> The "system model" and "software model" should be the same models, in my opinion. This is the approach we used in ERTMSFormalSpecs. " Thus you do not follow the phase by phase process recommanded by EN50126/50129/50128. I am interresting to know your arguments to justify this choice in regards of the development of a safety critical software.

" --> If you introduce a manual translation / manual verification by review step between the "system model" and "software model", then you loose verifiability of the Subset-026 model by domain experts. " Usually, domain experts are involved in this review.

stanpinteTheSignallingCompany commented 11 years ago

Le 7/02/2013 15:19, MariellePetitDoche a écrit :

--> The "system model" and "software model" should be the same models, in my opinion. This is the approach we used in ERTMSFormalSpecs. " Thus you do not follow the phase by phase process recommanded by EN50126/50129/50128. I am interresting to know your arguments to justify this choice in regards of the development of a safety critical software.

Dear Marielle,

Scrum is also not recommended by EN50126/50129/50128. That doesn't mean that everything not recommended by applicable EN norms is forbidden.

Of course, we have to justify our choice (which we have done in a Draft CENELEC 50128 ERTMSFormalSpecs white paper, available for review).

I did not received any principle arguments from our industrial customers pointing to the fact that having a same model for "system model" and "software model" for the OBU application software development would be against EN50126/50129/50128.

Could you please elaborate more, and point me to the exact requirements infringed?

Very kind regards

Stan


 Stanislas Pinte             e-mail: stan@ertmssolutions.com
 ERTMS Solutions               http://www.ertmssolutions.com
 Sales Director

 Follow us on twitter   http://twitter.com/#!/ertmssolutions

                                      Cell: +32 499 25 94 24
 Rue de la caserne, 45                Tel:  +322 - 612.41.70
 1000        Bruxelles                Fax:  +322 - 522.09.30

MariellePetitDoche commented 11 years ago

@ stanislas :

Scrum is also not recommended by EN50126/50129/50128. That doesn't mean

that everything not recommended by applicable EN norms is forbidden.

Of course, we have to justify our choice (which we have done in a Draft CENELEC 50128 ERTMSFormalSpecs white paper, available for review).

I did not received any principle arguments from our industrial customers pointing to the fact that having a same model for "system model" and "software model" for the OBU application software development would be against EN50126/50129/50128.

Could you please elaborate more, and point me to the exact requirements infringed?

No I have higher priority on items to produce to the project now to enter in the details of FormalSpec proposal and to anlayse in which items it cover or not the standard : look on Merlin report, QA plan for more details, or Cenelec training from all4Tech for more details.

But you can not mix a organization tool (like Scrum, which can be adapt to a safety critical process), with design and validation process especially defined in several phases, with phase reviews, in CENELEC EN5012*.

stanpinteTheSignallingCompany commented 11 years ago

Dear Marielle,

I understand your priorities.

I think it would be interesting to include as language & tools evaluation criteria a list of potential CENELEC EN50128 blocking points for each candidate.

Very kind regards

Stan

Le 7/02/2013 15:48, MariellePetitDoche a écrit :

@ stanislas :

Scrum is also not recommended by EN50126/50129/50128. That doesn't mean

that everything not recommended by applicable EN norms is forbidden.

Of course, we have to justify our choice (which we have done in a Draft CENELEC 50128 ERTMSFormalSpecs white paper, available for review).

I did not received any principle arguments from our industrial customers pointing to the fact that having a same model for "system model" and "software model" for the OBU application software development would be against EN50126/50129/50128.

Could you please elaborate more, and point me to the exact requirements infringed?

No I have higher priority on items to produce to the project now to enter in the details of FormalSpec proposal and to anlayse in which items it cover or not the standard : look on Merlin report, QA plan for more details, or Cenelec training from all4Tech for more details.

But you can not mix a organization tool (like Scrum, which can be adapt to a safety critical process), with design and validation process especially defined in several phases, with phase reviews, in CENELEC EN5012*.

— Reply to this email directly or view it on GitHub https://github.com/openETCS/requirements/issues/8#issuecomment-13238741.


 Stanislas Pinte             e-mail: stan@ertmssolutions.com
 ERTMS Solutions               http://www.ertmssolutions.com
 Sales Director

 Follow us on twitter   http://twitter.com/#!/ertmssolutions

                                      Cell: +32 499 25 94 24
 Rue de la caserne, 45                Tel:  +322 - 612.41.70
 1000        Bruxelles                Fax:  +322 - 522.09.30

MerlinPokam commented 11 years ago

Dear Sylvain, Dear Cyril,

Please find attached my answer!

The SRS SUBSET-026 is a system specification: it does not provide an internal architecture of the onboard subsystem;

--> of cause, the subset026 provide an internal architecture of the on board unit (see subset 026, Part 1, §2.5.3). This architecture is an abstract one, but still an architecture.

The SRS SUBSET-026 is a system specification: it does not clarify the Safety/Non Safety properties;

--> I agree.

The proposal would be to provide a subsystem requirement specification (SSRS) betwen SRS and the formal model.

--> I don't understand! Can you explain more?

The first purpose of this document will be to distinguish the onboard requirement from the trackside requirement.

--> we have already the onboard requirement (see subset026) and openETCS only address the onboard device. So why distinguish the onboard from the trackside?

The second purpose will be to provide the functional architecture of the OBU and OBU kernel.

--> I agree. We need a more concrete architecture

The second purpose will be to provide the functional architecture of the OBU and OBU kernel. It will clarify which part of the OBU will be in the model,

--> some part of the software will not be model?

I thought we wan to model the "entire" ETCS/ERTMS functionality

Downstream this document, we think that there is no need for a SwRS.

--> I do not agree! A software requirement specification is mandatory (according to EN 50128)

It is however clear that introducing a SSRS will lower slightly the level of the formal model: it is not a straight from the SRS to the model approach.

--> I can't follow you!

Best regards

Merlin Pokam

AEbt Angewandte Eisenbahntechnik GmbH Laufertorgraben 4 90489 Nürnberg

spätestens ab 05/2013: Adam-Klein-Str. 26 90429 Nürnberg

Tel. +49 911 52 09 92-172

FAX +49 911 52 09 92-10

merlin.pokam@aebt.de mailto:merlin.pokam@aebt.de www.aebt.de http://www.aebt.de/

AEbt Angewandte Eisenbahntechnik GmbH Geschäftsführer: Norbert Schäfer Sitz der Firma: Nürnberg Amtsgericht Nürnberg HRB 21962 USt-IdNr. DE237642651


Von: Sylvain Baro [mailto:notifications@github.com] Gesendet: Mittwoch, 6. Februar 2013 14:16 An: openETCS/requirements Betreff: [requirements] Is a SSRS needed between SRS and model? (#8)

We had a discussion (SNCF + Cyril Cornu) regarding the need of a document between the SRS and the formal model.

The SRS SUBSET-026 is a system specification: it includes onboard and trackside requirements; it does not provide an internal architecture of the onboard subsystem;

moreover t does not clarify the Safety/Non Safety properties. The proposal would be to provide a subsystem requirement specification (SSRS) betwen SRS and the formal model.

The first purpose of this document will be to distinguish the onboard requirement from the trackside requirement.

The second purpose will be to provide the functional architecture of the OBU and OBU kernel. It will clarify which part of the OBU will be in the model, and what will be the interface with the outer world. It will also provide the internal functional architecture of the model (Safe Braking Model, Localization, Mode management,...) and the interfaces between each functions. Eventually, it will provide an allocation of the requirement into the functions, and the tagging Safety/Non Safety of the requirements.

The requirements will need to be modified for two reasons: they will need to make use of the I/O identified in the functional architecture, and they will possibly need to be cut down in order to fit into the functions (some SRS requirement could possibly correspond to two SSRS subrequirements allocated to two functions).

Downstream this document, we think that there is no need for a SwRS. The model should be defined at the highest level possible, and the purpose is that the software part will be refined (or generated in some way) from the formal model. It is however clear that introducing a SSRS will lower slightly the level of the formal model: it is not a straight from the SRS to the model approach.

The pros:

The cons:

Reply to this email directly or view it on GitHub https://github.com/openETCS/requirements/issues/8 .

https://github.com/notifications/beacon/Jshd8sI44GVrKZBvymxqKL1MyGc6kA88c18k9C-l1L_G7q7tVmUWqDfHo3obja9R.gif

MERCEmentre commented 11 years ago

@MerlinPokam Merlin, you said: """ --> we have already the onboard requirement (see subset026) and openETCS only address the onboard device. So why distinguish the onboard from the trackside? """

If you look closely at the content of the SUBSET 026, you will see that some requirements are for the trackside part of the system.

To take just one example: "SUBSET 026-3 §3.5.3.9 When the trackside receives the session established report or the information that no compatible system version is supported by the on-board, it shall consider the communication session established."

This requirement is clearly only for the trackside and not for the onboard.

Best regards, david

MERCEmentre commented 11 years ago

@sbaro Sylvain, you said: """ What I had in mind was more like paper and natural language. Indeed, going down from system to subsystem is a step, and providing some internal architecture is another step. I think both these step could be combined in one (SRS -> SSRS) because they all deal with refining the requirement, chosing who is "in" and "out".

But (IMHO), introducing some formal language is another step (a big one), and I am not sure that it is a good idea to formalize in the same move than the refinement. """

In my view, for your SRS -> SSRS refinement, I was only thinking at refining the architecture of the model, i.e. the different functional parts of the SRS and their relationships. For me, the purpose of such an intermediate step is a better understanding of the SRS, as well as having a hierarchical view of the requirements. I am not considering any software architecture. Therefore, I think a software architecture step would be necessary after SSRS production.

Regarding the notation (paper & pencil, SysML, Event B, ERTMSFormalSpec or other), I have mixed feelings, seeing advantages and disadvantages to all of them. From my point of view, using a constrained notation (i.e. a well defined syntax, maybe with an informal semantics) would have a slight advantage of re-usability in later steps, but I might be wrong.

stanpinteTheSignallingCompany commented 11 years ago

Dear Sylvain, Dear David,

This is a very interesting discussion. However, do you already see how to translate what we discussed in high-level requirements that ould fit in our req_synthesis.tex doc?

To be honest, I don't see it yet :)

Very kind regards

Stan

Le 12/02/2013 15:01, David MENTRE a écrit :

@sbaro https://github.com/sbaro Sylvain, you said: """ What I had in mind was more like paper and natural language. Indeed, going down from system to subsystem is a step, and providing some internal architecture is another step. I think both these step could be combined in one (SRS -> SSRS) because they all deal with refining the requirement, chosing who is "in" and "out".

But (IMHO), introducing some formal language is another step (a big one), and I am not sure that it is a good idea to formalize in the same move than the refinement. """

In my view, for your SRS -> SSRS refinement, I was only thinking at refining the architecture of the model, i.e. the different functional parts of the SRS and their relationships. For me, the purpose of such an intermediate step is a better understanding of the SRS, as well as having a hierarchical view of the requirements. I am not considering any software architecture. Therefore, I think a software architecture step would be necessary after SSRS production.

Regarding the notation (paper & pencil, SysML, Event B, ERTMSFormalSpec or other), I have mixed feelings, seeing advantages and disadvantages to all of them. From my point of view, using a constrained notation (i.e. a well defined syntax, maybe with an informal semantics) would have a slight advantage of re-usability in later steps, but I might be wrong.

— Reply to this email directly or view it on GitHub https://github.com/openETCS/requirements/issues/8#issuecomment-13433461.


 Stanislas Pinte             e-mail: stan@ertmssolutions.com
 ERTMS Solutions               http://www.ertmssolutions.com
 Sales Director

 Follow us on twitter   http://twitter.com/#!/ertmssolutions

                                      Cell: +32 499 25 94 24
 Rue de la caserne, 45                Tel:  +322 - 612.41.70
 1000        Bruxelles                Fax:  +322 - 522.09.30

sbaro commented 11 years ago

@MerlinPokam : """ --> of cause, the subset026 provide an internal architecture of the on board unit (see subset 026, Part 1, §2.5.3). This architecture is an abstract one, but still an architecture. The SRS SUBSET-026 is a system specification: it does not clarify the Safety/Non Safety properties; """ What I had in mind was a more detailed functional architecture. In particular it could provide the "boxes&arrows" of the functions in the kernel (which is not the case of the architecture of subset 26. """ --> I don't understand! Can you explain more? The first purpose of this document will be to distinguish the onboard requirement from the trackside requirement. """ Yes, and to allocate the onboard requirements to the functions of the architecture. """ --> some part of the software will not be model? I thought we wan to model the "entire" ETCS/ERTMS functionality Downstream this document, we think that there is no need for a SwRS. """ I don' know. This has to be discussed. Is it realistic to provide all? """ --> I do not agree! A software requirement specification is mandatory (according to EN 50128) It is however clear that introducing a SSRS will lower slightly the level of the formal model: it is not a straight from the SRS to the model approach. """ It is not a problem I think. SwRS is required for a "traditional" development: SRS => SSRS => SwRS => code. Here we want to develop the model from SRS or SSRS (this is the point of this issue). But once the model is developed, code will be generated from it. So what is the use of a SwRS?

@MERCEmentre Regarding the architecture I agree with you. What I was on is the functional architecture, used to allocate the requirements and to help to grasp the system behavior. Software architecture (or model architecture) is another topic IMHO (and can be address in the design documentation).

Regarding the notation, I have no opinion on the one to be used for the architecure. But I think that the refined/allocated requirements must be provided at this step in natural language (this seems to be the main point of disagreement between Stan and I).

@stanpinte: I have some ideas... but I was in training these days. I have a version of my document ready, but I yet have to include your own comments, and the development of this issue.