AdaCore / RESSAC_Use_Case

A Collaborative Development Assurance Lab
6 stars 12 forks source link

Difference between aborted and cancelled #26

Open clairedross opened 7 years ago

clairedross commented 7 years ago

Hello Emmanuel,

At several places in the document, guarantees are defined for when the mission has been cancelled (6.6.3.B, 6.6.3.2.A, 6.7.3.2 E...). But in the output of the AV, a difference is made between missions cancelled and aborted. Could you explain what is the difference between a mission being cancelled or aborted and when each may occur?

Thanks in advance, Claire

ledinot commented 7 years ago

Canceled and Aborted have in common that the payload is not delivered. Canceled = “Aborted” or “stopped” before take-off. Aborted = “Aborted” or ”stopped” after take-off.

So there is a great difference: emergency landing in case of Aborted, no risk for the drone in case of Canceled.

De : Claire Dross [mailto:notifications@github.com] Envoyé : jeudi 29 juin 2017 15:11 À : AdaCore/RESSAC_Use_Case Cc : Subscribed Objet : [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Hello Emmanuel,

At several places in the document, guarantees are defined for when the mission has been cancelled (6.6.3.B, 6.6.3.2.A, 6.7.3.2 E...). But in the output of the AV, a difference is made between missions cancelled and aborted. Could you explain what is the difference between a mission being cancelled or aborted and when each may occur?

Thanks in advance, Claire

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweJ2So_bg0FATkMAkyS2C2fI6r7rvks5sI6J0gaJpZM4OJR9k.

clairedross commented 7 years ago

Hello Emmanuel, thanks for your answer. You said that cancelled was only done before the start of the mission, but then do 6.6.3.B, 6.6.3.2.A, and 6.7.3.2 E only apply on missions cancelled before take-off or also on aborted ones? Also, when is a mission 'cancelled' exactly? If start or go are received when the system is not ready (not enough energy, payload bay still opened, mission parameters not defined yet)? Thanks again, Claire

ledinot commented 7 years ago

Hi Claire,

It is applied for cancelled only, and intended to be extended to aborted missions when data recorders (Maintenance System) are added.

A guarantee has to be verifiable. Before take-off, “canceled” results from pure theoretical energetic computation, based on standard weather condition assumptions, or verifiable facts like failures, or bay still open etc. You can verify the correctness of this decision logic.

After take-off, what actually happened during flight matters to decide whether the guarantee was met or violated (e.g the abort of this mission was undue). With a flight data recorder (FDR) it will be hard to perform this kind of “post-abort analysis”, possibly motivated by an upset customer (“justify why this delivery failed”), but not impossible. Without an embedded FDR it is impossible.

A mission is cancelled at the end of the “booting sequence”: preparation of the systems, read/receive of the NAV parameters, viability computation by F_MM, wait for the bay to be closed etc. If Start/Go is received before the end of this “boot”, it is buffered until end of “boot”, i.e until it is possible do decide whether this command can be executed or not. If it is received after:

Sincerely, Emmanuel

De : Claire Dross [mailto:notifications@github.com] Envoyé : vendredi 30 juin 2017 11:16 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : [Message publicitaire : ] Re: [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Hello Emmanuel, thanks for your answer. You said that cancelled was only done before the start of the mission, but then do 6.6.3.B, 6.6.3.2.A, and 6.7.3.2 E only apply on missions cancelled before take-off or also on aborted ones? Also, when is a mission 'cancelled' exactly? If start or go are received when the system is not ready (not enough energy, payload bay still opened, mission parameters not defined yet)? Thanks again, Claire

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26#issuecomment-312218550, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweMGIBSZZBJRFXf2MqTz_T3_ZkOAlks5sJLzggaJpZM4OJR9k.

clairedross commented 7 years ago

Hi Emmanuel,

Le 03/07/2017 à 19:48, Emmanuel Ledinot a écrit :

It is applied for cancelled only, and intended to be extended to aborted missions when data recorders (Maintenance System) are added.

I must tell I am a bit surprised. When I read "Missions cancelled for energy reasons can be proven infeasible (under assumption of existence of an embedded MS flight data recorder for a posteriori analysis)" it really sound like this guarantee is only valid under the assumption of the presence of data recorders... Note that, even for in flight abortion, this is perfectly expressible (and verifiable) with contracts even without data recorders...

A mission is cancelled at the end of the “booting sequence”: preparation of the systems, read/receive of the NAV parameters, viability computation by F_MM, wait for the bay to be closed etc. If Start/Go is received before the end of this “boot”, it is buffered until end of “boot”, i.e until it is possible do decide whether this command can be executed or not. If it is received after:

  • either the boot ended with an F_MM status = “not viable”,so CANCELED is already lighted-on on CP, and the command is just ignored,
  • or the status is viable (+ bay closed etc. = READY lighted on), and the command is executed (beginning of take-off).

OK, so cancelled is not a terminal state, like aborted or completed, right? I mean, if GS changes the distance, then the mission will be viable and the state will go to ready? It is nothing more like the dual of ready, once the bay is closed and computation is done, either the ready light or the cancelled light is on and nothing more? Also, just to confirm, the READY light is not supported at this increment, is it?

-- Claire

ledinot commented 7 years ago

Hi Claire,

Your quote: I must tell I am a bit surprised. When I read "Missions cancelled for energy reasons can be proven infeasible (under assumption of existence of an embedded MS flight data recorder for a posteriori analysis)" it really sound like this guarantee is only valid under the assumption of the presence of data recorders...

The sentence you quoted legitimates your surprise, I agree. In a sloppy (or too quick) way of wording this part of the specification I used “Canceled” as synonymous of “Aborted”. But the context of the sentence clearly is that of post-mission analysis, and proof that a mission deemed infeasible actually was so. So flight, flight-data => ‘Aborted’ missions. ‘Canceled’ was inappropriately used because we are not addressing the pre-flight phase. A review of the spec to check use consistency of Canceled&Aborted has to be done.

OK, so cancelled is not a terminal state, like aborted or completed, right? I mean, if GS changes the distance, then the mission will be viable and the state will go to ready? It is nothing more like the dual of ready, once the bay is closed and computation is done, either the ready light or the cancelled light is on and nothing more? Also, just to confirm, the READY light is not supported at this increment, is it?

Yes it is not a terminal state (contrary to Aborted and Completed). Your scenario is OK (your dual view of ‘Canceled’ too).

The READY light is supported as early as increment 1. But its logic will be enriched by increment 3.

Suppose there is no GS (A mode), USB key has been read, viability computation said OK, the payload is in the bay but the door is not closed (it seems to be so, but is not really indeed). Then ‘Canceled’ is Off and ‘Ready’ as well. Thus the operator knows that the mission can be launched, but a “recoverable” squawk stopped the preparation phase, and that he has something to fix. READY says: “now please step a few meters back, take-off is pending”. CANCELED says: “the conditions were given, but there is stumbling block in them”. For instance (in A mode), everything was done appropriately but the USB key was not plugged-in. It does not trigger ‘Canceled’. It is like the bay door seemingly closed but not closed: it freezes the mission preparation “sequence”. Beware: any order (of preparation actions) has to be accepted. What matters is that in the end all the needed information(s)/action(s) have been provided/performed, and all the necessary (and sufficient) conditions for flight are satisfied. Something missing (still unknown, or not done but doable) is not equivalent to something known or done but incompatible with flight feasibility. In your example of GS modifying the distance, it is ‘Canceled’ and not ‘silent freeze’ because the distance was given, nothing more was expected from the operator.

De : Claire Dross [mailto:notifications@github.com] Envoyé : mardi 4 juillet 2017 12:46 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : Re: [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Hi Emmanuel,

Le 03/07/2017 à 19:48, Emmanuel Ledinot a écrit :

It is applied for cancelled only, and intended to be extended to aborted missions when data recorders (Maintenance System) are added.

I must tell I am a bit surprised. When I read "Missions cancelled for energy reasons can be proven infeasible (under assumption of existence of an embedded MS flight data recorder for a posteriori analysis)" it really sound like this guarantee is only valid under the assumption of the presence of data recorders... Note that, even for in flight abortion, this is perfectly expressible (and verifiable) with contracts even without data recorders...

A mission is cancelled at the end of the “booting sequence”: preparation of the systems, read/receive of the NAV parameters, viability computation by F_MM, wait for the bay to be closed etc. If Start/Go is received before the end of this “boot”, it is buffered until end of “boot”, i.e until it is possible do decide whether this command can be executed or not. If it is received after:

  • either the boot ended with an F_MM status = “not viable”,so CANCELED is already lighted-on on CP, and the command is just ignored,
  • or the status is viable (+ bay closed etc. = READY lighted on), and the command is executed (beginning of take-off).

OK, so cancelled is not a terminal state, like aborted or completed, right? I mean, if GS changes the distance, then the mission will be viable and the state will go to ready? It is nothing more like the dual of ready, once the bay is closed and computation is done, either the ready light or the cancelled light is on and nothing more? Also, just to confirm, the READY light is not supported at this increment, is it?

-- Claire

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26#issuecomment-312846987, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweE8pKxMIy95b2b35qhzLpNUtyyi0ks5sKhfxgaJpZM4OJR9k.

clairedross commented 7 years ago

Hi Emmanuel,

Thanks, it is much clearer indeed.

Le 04/07/2017 à 13:39, Emmanuel Ledinot a écrit :

A review of the spec to check use consistency of Canceled&Aborted has to be done.

One last question on this, when it is said in 6.6.3.B "Any mission cancellation is signaled to CP and GS." does it speak of cancellation, abortion or both?

The READY light is supported as early as increment 1. But its logic will be enriched by increment 3.

Here I am not sure I understand. I don't see anything for the ready state in the outputs of F_MM, and in 6.9.4 dispatch table there is a note for Ready reading "This register is not loaded at Increment 1". So here the ready light will never (or always) be on, right?

Thanks again for your help,

-- Claire

ledinot commented 7 years ago

Hi Claire, Q1 : Both. Q2 : why no « READY » output in F_MM ? Because I forgot it! To be coined * (or ** :-)). ICDs (Interface Control Documents) without behavioral modeling/design are doomed to be incomplete. To be added in 6.6.2.2 (F_MM) and in 6.9.4 (F_CM): output MissionREADY (along with MissionCANCELLED, MissionCOMPLETE, MissionABORTED). Q3 : note 8 explains to me why I forgot Mission READY. I thought that at increment 1 READY would systematically be On because resource failures do not exist, and so it was useless and needed to be discarded at this first stage. But that’s wrong, READY is needed anyway to notify the operator(s) that the drone can be launched (by START command).

WARNING: I was wrong when saying in my previous answer: READY implies pending automatic take-off. READY means: the “START button” becomes active (either from GS or by the operator at CP). This action triggers pending take-off (a few seconds later, the time needed to step back a few meters away from the drone).

De : Claire Dross [mailto:notifications@github.com] Envoyé : mardi 4 juillet 2017 14:59 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : Re: [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Hi Emmanuel,

Thanks, it is much clearer indeed.

Le 04/07/2017 à 13:39, Emmanuel Ledinot a écrit :

A review of the spec to check use consistency of Canceled&Aborted has to be done.

One last question on this, when it is said in 6.6.3.B "Any mission cancellation is signaled to CP and GS." does it speak of cancellation, abortion or both?

The READY light is supported as early as increment 1. But its logic will be enriched by increment 3.

Here I am not sure I understand. I don't see anything for the ready state in the outputs of F_MM, and in 6.9.4 dispatch table there is a note for Ready reading "This register is not loaded at Increment 1". So here the ready light will never (or always) be on, right?

Thanks again for your help,

-- Claire

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26#issuecomment-312871779, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweK4IwdU0uiX5BqEx0ENXERahS9qmks5sKjcggaJpZM4OJR9k.

clairedross commented 7 years ago

Hi Emmanuel,

this is much clearer now, thanks a lot.

-- Claire

ledinot commented 7 years ago

If clear enough to close, could you close (like Anthony does)?

De : Claire Dross [mailto:notifications@github.com] Envoyé : mardi 4 juillet 2017 18:15 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : [Message publicitaire : ] Re: [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Hi Emmanuel,

this is much clearer now, thanks a lot.

-- Claire

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26#issuecomment-312913365, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweD0Rc2b5LQPJzwJzk3QSGasRo4KUks5sKmUNgaJpZM4OJR9k.

clairedross commented 7 years ago

Le 04/07/2017 à 19:48, Emmanuel Ledinot a écrit :

If clear enough to close, could you close (like Anthony does)?

I think Anthony only closes issues when there is nothing to change in the document. But here, there are things to change, the ready output of F_MM, the clarification between cancelled and aborted? If you think there is nothing to do, I will indeed close the issue.

-- Claire

ledinot commented 7 years ago

I was not aware of this rule, which seems to me a good one. So yes, leave it open. E.

De : Claire Dross [mailto:notifications@github.com] Envoyé : mercredi 5 juillet 2017 09:34 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : Re: [AdaCore/RESSAC_Use_Case] Difference between aborted and cancelled (#26)

Le 04/07/2017 à 19:48, Emmanuel Ledinot a écrit :

If clear enough to close, could you close (like Anthony does)?

I think Anthony only closes issues when there is nothing to change in the document. But here, there are things to change, the ready output of F_MM, the clarification between cancelled and aborted? If you think there is nothing to do, I will indeed close the issue.

-- Claire

— You are receiving this because you were assigned. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/26#issuecomment-313025626, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweB2yVVfzyRrYQimVwPaeP2BnImqqks5sKzxpgaJpZM4OJR9k.

CyrilleComar commented 7 years ago

Le 05/07/2017 à 10:10, Emmanuel Ledinot a écrit :

I was not aware of this rule, which seems to me a good one.

I tried to describe it some time ago but that was too complex, I'll send a simpler set of rules for document reviews to the RESSAC group soon.

So yes, leave it open.

my advice is to make the changes in the doc as soon as possible after the resolution has been agreed upon (informally) so that you remember the discussion (if any) when doing the change and you can close the opened issue quickly.