search

AdaCore / RESSAC_Use_Case

A Collaborative Development Assurance Lab
6 stars 12 forks source link

Mission_Cancelled input for F_FC #23

Open clairedross opened 7 years ago

clairedross commented 7 years ago

Hello Emmanuel,

In 6.7.3.1.C (assumption of F_FC) it is said that "Every mission is viable or cancelled". I do not quite understand this assumption for two reasons. First, I don't know how to express it as F_FC has no Mission_Cancelled input from F_MM. Second, I don't understand what it is used for in the behavior of F_FC? Maybe this is only needed for global system level properties like Guarantees 6.7.3.2 A, B, and C because they cannot be ensured if there is no energy left?

Thanks for your inputs, Claire

ledinot commented 7 years ago

In 6.7.3.1.C (assumption of F_FC) it is said that "Every mission is viable or cancelled". I do not quite understand this assumption for two reasons. First, I don't know how to express it as F_FC has no Mission_Cancelled input from F_MM.

You can create it if you need it. I didn’t feel that need, contrary to that of MissionAborted.

I considered that F_FC is launched by F_MM when a mission has to be performed, and is not activated otherwise, instead of considering that F_FC is running on ground anyway (but needlessly anyway as well), and that a signal has to be sent (MissionCancelled) to stop it.

Second, I don't understand what it is used for in the behavior of F_FC? Maybe this is only needed for global system level properties like Guarantees 6.7.3.2 A, B, and C because they cannot be ensured if there is no energy left?

This garantee is not needed for F_FC. It is needed for the clients.

Any take-off doomed to end by an emergency landing (instead of smooth parcel delivery :-)), is an opportunity to lose the drone.

Sincerely,

Emmanuel

clairedross commented 7 years ago

You said that Mission_Aborted is needed, but I don't see it either in the inputs of F_FC. Is it needed then?

ledinot commented 7 years ago

Claire,

Sorry for having overlooked this one (and seemingly a few other ones) .

Mission_Aborted is not (necessarily) needed in the inputs of F_FC. F_MM is supervision, the boss, the master. I implicitly assumed (I acknowledge the implicit aspect) that F_MM would deactivate F_FC. This comes from my synchronous reactive programming bias (hierarchical state machines can perform instantaneous external kill actions on other tasks).

F_MM can send “Mission_Aborted” to F_FC, as a command for F_FC to commit self-deactivation (suicide). But with modeling/implementing by means of hierarchical state machines such a signal is not needed.

To be coined ** for the lessons learnt. It shows that even at very high level (system/functional/textual) mental concepts, i.e implicit frames of mind, have influence on as basic specification entities as functional interfaces. In other words, specifying (at system level) without having some influence on design at software level (choice of the interfaces), is very hard, and possibly impossible.

Cheers, E.

De : Claire Dross [mailto:notifications@github.com] Envoyé : mercredi 28 juin 2017 10:12 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Assign Objet : Re: [AdaCore/RESSAC_Use_Case] Mission_Cancelled input for F_FC (#23)

You said that Mission_Aborted is needed, but I don't see it either in the inputs of F_FC. Is it needed then?

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