search

AdaCore / RESSAC_Use_Case

A Collaborative Development Assurance Lab
6 stars 12 forks source link

Guarantees: Missions cancelled for energy reasons can be proven infeasible but not the opposite #7

Open AnthonyLeonardoGracio opened 7 years ago

AnthonyLeonardoGracio commented 7 years ago

Document: UseCaseDevelopment/Layer1_MMS/RESSAC_muXAV_SystemRQ_MMS_SW_Incr1.doc Commit: 74aa074

On doit prouver qu’une mission annulée était bien infaisable : pas l’inverse ?

Réponse initiale

Si bien sûr. C’est un oubli de ma part dans la partie Guarantee du contrat : SAFETY : si la mission est énergétiquement infaisable, on ne lance pas le drone pour faire emergency landing ensuite (même soft), éventuellement sur un marché ou une école maternelle … AVAILABILITY : on n’annule pas intempestivement. Donc au final c’est bien l’équivalence qu’il faut.