Velo - Vérification pour l'Environnement et le LOgiciel

CR 23/12/2008 (rédigé par MM)

Présents : PA, CA, MM.

Points discutés :

• Portée des variables d'état d'un composant :

  • OBSERVABLE : c'est un ensemble de noms de variables (⊆ VARIABLES) par défaut vide,
    

    * Les OBSERVABLE peuvent être utilisées dans les assertions de service,
    * Les OBSERVABLE peuvent être utilisées dans les [propriétés] du composant,
    * Les OBSERVABLE peuvent être utilisées dans l'invariant du composant,
    * La promotion [des variables] par renommage porte sur les OBSERVABLE uniquement (cohérence ⇒ non modifiables),
    * Au niveau d'un service offert, on utilise un sous-ensemble de variables dans OBSERVABLE qui sont présentes dans les Pré/Post (Os ⊆ Oc),
    * Un service requis peut (en plus de ses paramètres) supposer un contexte d'appel composé de variables [observées],
    * Les variables observées devront correspondre à des variables observables du composant qui offre le service.

  1. Règles imposées (sauf pour une nouvelle motivation particulière):

  • Pas de distinctions entre composition et assemblage (en terme de visibilité des varables),
  • Pas de liens entre composants mais entre services (en terme d'accès aux variables observables),
  • Pas de variables observables du composant qui définit le service requis dans les Pré/post de ce dernier ( ⇒ garde), l'idée c'est de voir un service requis seulement comme une image du service offert.
• Plan de SC'09
  • A voir sur le CVS

    • 4 niveaux
      1. Signature
      2. Structure
      3. Assertion + Contexte (ce qui devrait être traité dans SC'09)
      4. Behavior
         

    1. Présentation rapide du CR sur le projet Miles (faite pas CA).

    PS : Je mettrais plus tard des photos (peut-être) plus claires pour les schémas.