AdaCore / RESSAC_Use_Case

A Collaborative Development Assurance Lab
6 stars 12 forks source link

Safety envelope in F_FC #18

Open clairedross opened 7 years ago

clairedross commented 7 years ago

Hi again, Here is a new question, sorry for flooding... In the guarantees of F_FC (6.7.3.2.C) it is stated that F_FC must guarantee that the AV is kept in flight safety envelope, which are expressed as bounds on p, q, pdot and qdot. I am not completely sure of what it means. Indeed, p, q, and pdot are inputs of F_FC (and qdot is not even an input as it is not measurable), how is F_FC supposed to be able to guarantee that bad values of its inputs will not occur? Or maybe it is the definition of safety escape in 6.7.3.2.E and F_FC is only responsible for launching emergency landing if these properties are violated too often? Thanks for your help, Claire

ledinot commented 7 years ago

how is F_FC supposed to be able to guarantee that bad values of its inputs will not occur?

Interesting. That’s an issue to be ***-coined for later “lessons learnt” analysis (it exemplifies the difference of mindset between system/control engineers, and software engineers).

F_FC influences its inputs (p, pdot, q) “indirectly”, by closed loop interaction through physics. The torque commands that F_FC computes, act on the AV’s body, whose mechanical state is sensed (-> (p, pdot, q)), received by F_FC. The P,I,D constants and the grids are tuned to ensure the guarantees on p, pdot,q, qdot, whatever wind gusts the drone will be subjected to (assuming they are within appropriate/certifiable bounds however).

De : Claire Dross [mailto:notifications@github.com] Envoyé : jeudi 22 juin 2017 16:46 À : AdaCore/RESSAC_Use_Case Cc : Subscribed Objet : [AdaCore/RESSAC_Use_Case] Safety envelope in F_FC (#18)

Hi again, Here is a new question, sorry for flooding... In the guarantees of F_FC (6.7.3.2.C) it is stated that F_FC must guarantee that the AV is kept in flight safety envelope, which are expressed as bounds on p, q, pdot and qdot. I am not completely sure of what it means. Indeed, p, q, and pdot are inputs of F_FC (and qdot is not even an input as it is not measurable), how is F_FC supposed to be able to guarantee that bad values of its inputs will not occur? Or maybe it is the definition of safety escape in 6.7.3.2.E and F_FC is only responsible for launching emergency landing if these properties are violated too often? Thanks for your help, 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/18, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweO5F8RBsEPyfAH_n4iwrjzi9Puerks5sGn4pgaJpZM4OCZyv.

clairedross commented 7 years ago

OK, so those are more like invariants or range constraints on p, q, and pdot (and qdot, but I am not sure what to do with these ones). I don't see how we could verify that they are preserved by our system though, since it must certainly depend on the physical behavior of the drone. Also, are these contraints always verified or only in SWC?

ledinot commented 7 years ago

F_FC has two parts :

  1. command (-> the torques) and

  2. monitoring (the alerts “safety escape!!!”).

OK, so those are more like invariants or range constraints on p, q, and pdot (and qdot, but I am not sure what to do with these ones). I don't see how we could verify that they are preserved by our > system though, since it must certainly depend on the physical behavior of the drone. Also, are these contraints always verified or only in SWC?

Yes they are invariants to be ensured, they are the expected safety guarantees (so take care ….! :-)). But, … even if the software is correct, and PID coefficients’ calibration is correct (PDI affairs, PDI for PID, everything OK ?:-)), these so called “invariants” may be broken … For instance a wind blast beyond SWC...

De : Claire Dross [mailto:notifications@github.com] Envoyé : jeudi 22 juin 2017 17:08 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Comment Objet : [Message publicitaire : ] Re: [AdaCore/RESSAC_Use_Case] Safety envelope in F_FC (#18)

OK, so those are more like invariants or range constraints on p, q, and pdot (and qdot, but I am not sure what to do with these ones). I don't see how we could verify that they are preserved by our system though, since it must certainly depend on the physical behavior of the drone. Also, are these contraints always verified or only in SWC?

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/18#issuecomment-310408895, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVweKryUMLsdCWTrqJypx6k4mjGN_Krks5sGoNJgaJpZM4OCZyv.

clairedross commented 7 years ago

All right, so is the violation of these invariants what is called a safety escape in 6.7.3.2.E?

ledinot commented 7 years ago

Yes indeed.

De : Claire Dross [mailto:notifications@github.com] Envoyé : jeudi 22 juin 2017 17:26 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Comment Objet : Re: [AdaCore/RESSAC_Use_Case] Safety envelope in F_FC (#18)

All right, so is the violation of these invariants what is called a safety escape in 6.7.3.2.E?

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/18#issuecomment-310414389, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVwePvMvE_aOmi-ObcU6F488bfqm8HBks5sGoeXgaJpZM4OCZyv.

ledinot commented 7 years ago

Yes, indeed.

De : Claire Dross [mailto:notifications@github.com] Envoyé : jeudi 22 juin 2017 17:26 À : AdaCore/RESSAC_Use_Case Cc : Ledinot Emmanuel; Comment Objet : Re: [AdaCore/RESSAC_Use_Case] Safety envelope in F_FC (#18)

All right, so is the violation of these invariants what is called a safety escape in 6.7.3.2.E?

— You are receiving this because you commented. Reply to this email directly, view it on GitHubhttps://github.com/AdaCore/RESSAC_Use_Case/issues/18#issuecomment-310414389, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AVVwePvMvE_aOmi-ObcU6F488bfqm8HBks5sGoeXgaJpZM4OCZyv.

clairedross commented 7 years ago

Thank you for your answers.