Project for the course Conception Formelle

Gilles

• Rôle Makefile
  • Autres règles
  • Finir d'expliquer la règle tank.time
• Rôle de la constante nbFailures.

Gilles

Interprétation, c'est-à-dire, expliquer pour chaque ensemble à quoi cela corresponds en terme de propriétés, etc...

• Inteprétation des résultats avec 0 défaillances
• Inteprétation des résultats avec 1 défaillances
• Inteprétation des résultats avec 2 défaillances
• Inteprétation des résultats avec 3 défaillances
• Bilan avec le contrôleur initial

  Déterminer les limites du contrôleur (à partir de quand ça crash, etc...), dire ce qui marche et ce qui ne marche pas..

Gilles

• Expliquer la sémantique et le rôle du composant ValveVirtual
• Expliquer les mécanismes mis en oeuvre, leurs rôles et les avantages de ce contrôleur par rapport au précédent CtrlVV.

Gilles

Interprétation, c'est-à-dire, expliquer pour chaque ensemble à quoi cela corresponds en terme de propriétés, etc...

• Inteprétation des résultats avec 0 défaillances
• Inteprétation des résultats avec 1 défaillances
• Inteprétation des résultats avec 2 défaillances
• Inteprétation des résultats avec 3 défaillances
• Bilan avec le contrôleur CtrlVV

  Déterminer les limites du contrôleur (à partir de quand ça crash, etc...), dire ce qui marche et ce qui ne marche pas..

Emile

• Expliquer en quoi consiste l'optimisation mise en place
• Inteprétation des résultats avec 0 défaillances
• Inteprétation des résultats avec 1 défaillances
• Inteprétation des résultats avec 2 défaillances
• Inteprétation des résultats avec 3 défaillances
• Bilan avec l'optimisation du contrôleur CtrlVV

  Déterminer les limites du contrôleur (à partir de quand ça crash, etc...), dire ce qui marche et ce qui ne marche pas..

Emile

• Implémenter une des optimisation proposée pour CtrlVV
• Décrire les résultats obtenus après optimisation

Potentiellement, répéter les deux points précédents pour la deuxième optimisation proposée.

Emile

• Ecrire une conclusion finale sur la synthèse de contrôleur.