-
Notifications
You must be signed in to change notification settings - Fork 20
Open Question for Modeling Benchmark
Here, the open questions for the modeling of the benchmark can be collected. Such questions may arise from different sources: problems in the spec, insufficient requirements for a certain benchmark case etc.
The transitions have the same priority, the spec states that in this case "it is obvious that these transitions cannot occur at the same time". Nevertheless, just modeling the conditions [5], [6], [50] and [10] does not ensure mutual exclusion of the activation conditions.
The problem seems to be that in [10] "no specific mode is required by a Mode Profile" implicitly holds when shunting mode is selected or a shunting request is granted (to be confirmed).
This was found via a non-provable invariant in Event-B (mutual exclusion of the conditions) and was confirmed by David Mentré in the Why3 and GNATProve models.
Answer [laurent@ertmssolutions.com]
The problems with this finding is due to the incomplete modeling of the system, I will provide a proof of the mutual exclusion between conditions [5], [6], [50] and [10]. (see below and correct me if I am wrong).
I think that mutual exclusion is very difficult to prove when considering only part of the model, and strongly suggest the help of an ERTMS expert to determine the requirements that need to be taken into account for the proof.
Section 4.4.8.1.6 indicates that SH can be selected by the driver, only accepted when the train is at standstill, or ordered by the Trackside. More precisely, there are only three procedures that allow to change from SB to SH, namely
- Start of mission (section 5.4)
- Shunting initiated by driver (section 5.6)
- Entry in Shunting with Order from Trackside (section 5.7)
We shall analyze all these cases and prove that mutual exclusion is always respected.
Condition [50] corresponds to transition E33 in procedure Start of Mission. This is a special case for Procedure Shunting From Trackside which shall be analyzed below.
Condition [5] corresponds to transition E12 in procedure Start of Mission, followed by transition from D020 to A050 in procedure Shunting Initiated by Driver.
- Section 4.10.1.3 indicates that the MA has been removed when entering SB. No MA is available.
- Section 4.4.7.3.1 indicates that, in SB mode, the ERTMS/ETCS on-board equipment is responsible for maintaining the train at standstill.
- Since the train is at standstill, and the level is 0, 1 or NTC, no MA can be received
- MA can never be available in S10. This condition is mutually exclusive with Condition [10].
- => Mutual exclusion proven
Condition [6] corresponds to transition E12 in procedure Start of Mission, followed by transition E090 in procedure Shunting Initiated by Driver.
- Section 4.10.1.3 Indicates that the MA has been removed when entering SB. No MA is available.
- Since no MA request has been sent, no MA can be received. MA request is sent from S20, and there is no path from S20 to S10.
- MA can never be available in S10. This condition is mutually exclusive with Condition [10].
- => Mutual exclusion proven
Condition [50] corresponds to procedure Entry in Shunting with Order from Trackside.
- Paragraph 5.7.1.3 indicates that the order to switch to SH mode shall be given by means of a mode profile. This condition is mutually exclusive with Condition [10].
- => Mutual exclusion proven
Thanks, this confirms that for Section 4.6 and the selected transitions there is indeed some implicit dependency which is not directly reflected in the single conditions explained there.
In my opinion we should document this in the description of the case studies. I will add this as hypothesis to the model to prove the mutual exclusion of the conditions.
There are at least two unmentioned feedback loops in the Block-Diagram Figure 28 §3.13.1.3.
-
"Calculation of decelerations" need for calculation of A_save the EBD_foot from Module "Determination of brake deceleration curves" -> EBD_foot is an end condition for evaluating track condition (§3.13.6.2.1.5)
-
"Determination of brake deceleration curves" needs for EBDs regarding ceiling speed limits the EBI of "Supervision limits" -> the EBI is needed to calculate the EBD_foot (§3.13.8.3.1)
consequently also "Supervision limits" have a indirect feedback to "Calculation of decelerations"
Take care that figure 28 is only an overview not a Block-diagram figure, thus it shall not be exhaustive (there are no requirements linked to this figure). Besides on the left, there is an input arrow "Train position/ speed / acceleration" : no details are given on these inputs but we can imagine that there are the last values computed by the functions of "Speed and Distance Monitoring". System analyses shall clarify the inputs and outputs of these functions.
The description of the Figure 28 is "Figure 28 gives an overview of the main elements contributing to the speed and distance monitoring", so I agree with Marielle on the fact that this figure shall not give the detailed explanation of each "block" of this diagram. But I think that the links between these blocks should be clearly identified, otherwise it could lead to the misunderstanding of the specification. And actually the first example of missing feedback loop raised a lot of questions (see the following bug report). So I think that these two feedback loops are important and should be added to the figure.
This paragraph describes how the time until full brake contribution is reached. When calculating the corresponding deceleration A_safe, the track condition (especially prohibiting of special brakes) should be taken into account. But when calculating brake build up time only the status of special brakes are considered.
In my opinion this is a inconsistency. Either only the status of ep-brake should be considered, which is track independent(as far as I know), or also the applicable track conditions at d_est_front should be taken into account.