Review of D4.2.1 (TWT)

[srieger]

Section 1 (Institut Mines-Télécom)

Introduction

• Clearly state that the actual modelling in WP3 has not started yet to indicate that we have currently no "real" input.

1.3.1 Modeling decisions

• You state that normally a system is described by formulae which in my opinion is not true. I think there might be a confusion, as the requirements are formalised as formulae that are then model checked against the system descriptions (e.g., as automaton).
• Description of the messages depicted in Figure 1 is missing
• "The second aspect is related to the situation when, for some reason, exchange messages are lost. In order to deal with this situation we augment our model with timeout functions. If there is no input before the timeout expires then the player (RBC, a train under control, and/or the environment) has to make their own decision and for the safety issues usually it is the decision to stop the train." I believe that timeouts are mentioned only rarely in the standard. Do you have any indication of underspecification here? Especially it seems that in the standard lost messages do not seem to be taken into account properly in every situation.
• Your model of train and RBC is very rough. Did you check whether it is conformant to the standard? How did you derive it?
• Where in the standard can I find the safe position requirements stated on page 9? Please add a reference.

Section 1.3.2

• Write out abbreviations as ETFSM and EFSM at least once. Their meaning is not clear to me.
• To me the purpose of the simulator is not clear. It seems to use an XML-based language while IF and SysML languages are considered for model checking
• How do you transform SysML models to Promela?

Sections 1.4, 1.5 and 1.6

• Section 1.4.1: How did you derive those requirements? The title of the section seems to be a bit misleading as the process of derivation is not described.
• To me this section seems like a collection of possible verification techniques and corresponding tools. Some you applied to your example models (the testing techniques). Which ones did you apply/do you plan to apply in the future in WP4?

Section 1.7

• You state: "The model is a very close representation of the system specification provided by the standard." I strongly disagree. You have a model at a extremely high level of abstraction; the reference to the standard (from which parts did you extract your model) is missing.

General remarks

• I believe, that your model can be seen as demonstration that your proposed methods work or maybe even how they could be applied in the context of openETCS. But you should align with the other partners and go much more into detail when you specify a real test model.
• Provide your (preliminary) results and models via GitHub, e.g., create a user story as other partners have done.
• I found some spelling/grammar mistakes, please recheck.

[srieger]

151

[srieger]

Section 3 (Uni Bremen)

Goals

• "Our main goal is to validate the SCADE model by test simulation. The tests are produced by a model of the subset-026 chap 3.5 described as a state machine." You probably intend verification by test execution or am I wrong?

Method/Approach

• What happens if your test model is too abstract, e.g., in the extreme case it could be the automaton with a single state that can do everything? Clearly all possible paths are available then.
• You should stress that both models are created manually independent from each other.
• "We need then to link the system under test and the test model. [...]" Could you add details here? In my understanding you need a link to be able to feed the generated test cases to the code and the result back, is this right?
• As your generate test cases from an abstract model according to a certain coverage strategy, I assume that if you have full coverage in the test model, this does not imply the same for the code, right?
• The purpose of the LTL formulae is not entirely clear to me. Maybe add more details

Results

• The heading "Test cases covered" in Table 1 is somehow misleading as these are coverage criteria.
• More details and a description of Table 1 would be nice. What do these numbers imply?

Conclusions/Lessons learned

• Did you document the deficiencies in the specification? We started to document all issues we found to clarify them with railway experts and eventually improve the standard in the future.

General remarks

• I found some spelling/grammar mistakes, please recheck.

[srieger]

Section 4 (Uni Rostock)

Method/Approach

• You mention traceability, do you already have an idea on how to establish the link?

Means

• You should improve the distinction between the SystemC model created by hand and the one derived from SysML. Call it "Generated Model" or something similar. This refers to the second bullet point.

Results

• Could you already derive an implications from the first simulation and performance evaluation runs?

Future Activities The following comment addresses not the authors but the consortium in general:

• Why did nobody consider Simulink as well? It is closed source as Scade is. Is it for certification reasons? In our company Simulink is used in various projects.

[srieger]

Section 5 (Systerel)

Model Checking

• Maybe you should mention that Model Checking involves the exhaustive exploration of the state space of the model. This does not become clear in your description
• "unability to run through all of the states and transitions" This is true if there are infinitely many, otherwise not. The idea of MC is to do exactly that.

Formal Proof

• How do you specify properties to be verified? They are proof obligations as well and not generated by the POG.
• "A proved model will always meet the safety and security qualifications ; however that doesn’t mean it will behave in regards to the specification! This is the domain of validation, as discussed in the introduction." Not clear to me what you mean by that. Verification is checking whether the implementation meets the specification while validation is checking whether the Specification is correct.

ProB

• Why has nobody brought this in the project? I mean especially @jastram, not the authors.

Table 2

• A more detailed explanation would be nice.

Formal proof results

• "Proving the model results in the certainty of its correctness." This is true, but with respect to the verified properties.
• You mention you checked only type-based properties, so what is the additional benefit with regards to a type-check.

Model-Checking of Predicates

• "In practice, tools like ProB which allow for model-checking of Event-B models, limit the size of the possible values for variables to a finite subset. While this means that a correct proof is not possible" Replace correct with complete

Object of Verification

• Why do you consider a different part of the standard here? Above you mentioned the procedure On-Sight.

Result

• "The requirements are formalized as invariants in predicate logic, their proofs are for the most part fully automatic." Which requirements? The requirements in the specification or your derived safety requirements?

Verification processes applicable to a SCADE model

• What about the Scade Prover?
• Here you are only at process level in contrary to B part. The basic process should be similar for Scade and B if you consider the different roles (e.g., verifier) or the reporting etc.

[nhnghia]

Dear Stefan, 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.

Introduction Clearly state that the actual modelling in WP3 has not started yet to indicate that we have currently no "real" input. 1.3.1 Modeling decisions

You state that normally a system is described by formulae which in my opinion is not true.

We would like to talk about existing modeling approches that described the system as formula.

Description of the messages depicted in Figure 1 is missing

We added this in our new version

"The second aspect is related to the situation when, for some reason, exchange messages are lost. In order to deal with this situation we augment our model with timeout functions. If there is no input before the timeout expires then the player (RBC, a train under control, and/or the environment) has to make their own decision and for the safety issues usually it is the decision to stop the train." I believe that timeouts are mentioned only rarely in the standard. Do you have any indication of underspecification here? Especially it seems that in the standard lost messages do not seem to be taken into account properly in every situation.

Your model of train and RBC is very rough. Did you check whether it is conformant to the standard? How did you derive it?

Where in the standard can I find the safe position requirements stated on page 9? Please add a reference.

As you said above, currently there is no real input and our model is somewhat abstract. We need to refine it in the next steps, e.g., the lost messages may happened when a train functions in Limited Supervision mode (Subset 26-4.4.19.3.1.1) or in Staff Responsible mode (Subset 26-4.11.1.2), timeout values can be used in Movement Authority (Subset 26-3.8), etc.

Write out abbreviations as ETFSM and EFSM at least once. Their meaning is not clear to me.

We added their descriptions.

To me the purpose of the simulator is not clear. It seems to use an XML-based language while IF and SysML languages are considered for model checking

Currently the simulator is generated from a XML description. We are studying to generate it from a SysML description that is also contained in an XML-based specification. The simulator is used to run some tests. It may be useful when we need to check some property againist a model in some specific condition since model-checking checks exhaustively the model. Thus Simulation-based testing can be considered as a low-cost solution to check a model (against some test cases)

How do you transform SysML models to Promela?

In fact, we are trying to use IFx model-checker to check IF specification, hence a translation from SysML models to IF models are beeing studied rather than to Promela.

To me this section seems like a collection of possible verification techniques and corresponding tools. Some you applied to your example models (the testing techniques). Which ones did you apply/do you plan to apply in the future in WP4?

We have reformulated this section.

Section 1.4.1: How did you derive those requirements? The title of the section seems to be a bit misleading as the process of derivation is not described.

You state: "The model is a very close representation of the system specification provided by the standard." I strongly disagree. You have a model at a extremely high level of abstraction; the reference to the standard (from which parts did you extract your model) is missing.

I believe, that your model can be seen as demonstration that your proposed methods work or maybe even how they could be applied in the context of openETCS. But you should align with the other partners and go much more into detail when you specify a real test model.

Currently, our model is somewhat abstract. It will be refined in the next steps, e.g., our Moving mode can be refined into TRIP mode of OBU, or Stop mode to System Failure mode, ...

Provide your (preliminary) results and models via GitHub, e.g., create a user story as other partners have done.

We are going to do that.

[srieger]

Dear @nhnghia ,

thank you very much for your response to my comments. To me it clarifies a lot and helps me to understand your approach.

[mgudemann]

Dear @srieger,

I included many of your comments in the changes at the PR https://github.com/openETCS/validation/pull/179

You mention you checked only type-based properties, so what is the additional benefit with regards to a type-check.

In B, typing invariants have to be explicit. In addition, it is possible to specify dependent types which are not analyzable using simple type checking. This is why these invariants exist.

Why do you consider a different part of the standard here? Above you mentioned the procedure On-Sight.

The B-model covers the on-sight procedure. While I also developed an Event-B model for this, I presented another case-study for the Event-B model as safety properties had been identified for this section of Subset 026. This allowed for giving direct examples for the different V&V aspects.

What about the Scade Prover?

SCADE Prover only allows Boolean "is never true" safety properties. This requires more complex formalization than using set-theoretic predicates or temporal logic of other model checkers and is less expressive. Note also, that the prover is not part of the certified aspect of SCADE.

I hope this clarifies your comments and questions.

[MariellePetitDoche]

@srieger:

"Formal Proof

How do you specify properties to be verified? They are proof obligations as well and not generated by the POG."

Properties to verify are specified by Invariant or pre or post conditions of operations. Then as they are specified, POG are automatically generated to verify them.

""A proved model will always meet the safety and security qualifications ; however that doesn’t mean it will behave in regards to the specification! This is the domain of validation, as discussed in the introduction." Not clear to me what you mean by that. Verification is checking whether the implementation meets the specification while validation is checking whether the Specification is correct." This means the modelled is only verified (ie. each level of the Bmodel or the implementation verify a more abstract one, a specification, is meets) but not validated (ie. we are not ensure the most abstract specification is correct in regards of an informal specification).

"You mention you checked only type-based properties, so what is the additional benefit with regards to a type-check." Only type-based properties as invariant, however function behaviour are specified (see .ref component in our VnV User story) thus it is proved that the implementation of a function verified the specified functional behaviour.

"What about the Scade Prover?" Which tool do you mean, there exists a model-checker for SCADe model, but obviously not open-source so we have prefered not to use it for the project.

"Here you are only at process level in contrary to B part. The basic process should be similar for Scade and B if you consider the different roles (e.g., verifier) or the reporting etc." Indeed some verification are common, however, formal verification can currently be stronger and more generic with open-source or free of charge tools with B method than with Scade.

[MarcBehrens]

Review closing session 19.3.2014: Comment on review for section 3 pending @cecilebraun .

[cecilebraun]

Sorry for the delay and thanks @srieger :

What happens if your test model is too abstract, e.g., in the extreme case it could be the automaton with a single state that can do everything? Clearly all possible paths are available then.

The test generator will of course generate test for what we had modelled only. If the test model is too coarse If the model is too abstract it can happens the following:

• The test failed :
  • either because the test model is too abstract and the test proposed does not correspond to any possible execution in the implementation, we then need to refine the test model
  • or there is a real bug

As your generate test cases from an abstract model according to a certain coverage strategy, I assume that if you have full coverage in the test model, this does not imply the same for the code, right?

The use of the different test strategies will ensure a better coverage of the code but of course full coverage on the test model does not imply full coverage on the implementation. Results

Did you document the deficiencies in the specification? We started to document all issues we found to clarify them with railway experts and eventually improve the standard in the future.

This an ongoing work with Uwe Steinke. I will be interested to know where I can help providing this deficiencies.

[MarcBehrens]

Review closing session 02.4.2014: Issue closed, please reopen if there is something missing.