photo tableau

• au niveau modele et non meta

• périmètre du test variable (schéma avec bouchons à la place d'un service interne ou non)
• sources de données non bornées

  •  (éventuellement composites, random) 
    *  (peuvent interroger leur environnement pour s'adapter eg. évaluer des assertions qu'elles doivent satisfaire)
    *  (difficulté : stratégies d'ordonnancement des sources appelées)

• états
• traces
• assertions
• exceptions
• résultat (retour)

• pass/fail/irrelevant
• responsabilité ( programme, source de donnée)
• confiance (exception lourde (div/0), assertions, boucle inf …)

• validation du prog/ sources données
• Validation des cas de test par mutation ( pas de comparaison des traces, par exemple)
• test de non régression (pas de comp de traces non plus, contrats éventuellement altérés) ⇒ sens des implications

: contrat <> oracle : oracle = CP (contrat du programme) + CT (contrat spécifique au cas de test).

CP n'a pas vocation à être améliorée si ce n'est après avoir corrigé une erreur. CT (initialement vide ou remplie manuellement) peut être améliorée suite à l'analyse de mutation.

Pour des raisons de généralité, d'ouverture (le composant n'est pas dans un monde clos), et de substituabilité, il est normal de sous-spécifier les contrats de CP (alors que les CT doivent être les plus précis possibles pour être efficaces)

• niveau modèle
• opérateurs classiques,
  • sur les expressions ( variables et fonctions à signatures compatibles)
  • sur les communications ( substitution comm ↔ fonction)
• opérateurs sur le LTS
  • complexes correspondant à une faute et construit sur des élémentaires
  • les simples génèrent trop d'erreurs sans intérêt : détectées “à la compil” et coûteuses à générer

partir de fautes plutôt que d'opérateurs élémentaires pour tenter de réduire l'explosion combinatoire

voir, pour référence, la page sur la génération de code java

Attention : gros brouillon en vue …

• la cohérence des exécutions d'un service avec la Post et l'Invariant
  * l'unité de test est le service (attention au contexte nécessaire à son exécution)

⇒ les post sont des oracles (elles sont donc supposées correctes (jusqu'à l'analyse de mutation?) ) l'échec d'un test signifie donc que - la pre n'est pas suffisante pour assurer la post, ou bien que le déroulement possède une erreur

• des modèles Kmelia
• de code Java permettant d'initialiser un composant et d'exécuter un service (pour l'instant avec des bouchons pour les communications)
• les services peuvent dire si leur pre est vérifiable, et si oui, si des données la satisfont (partiellement pour les requis actuellement)
• les services peuvent dire si leur post est vérifiable, et si oui, si des données la satisfont (faux pour les requis)
• les services ne modifient pas leurs paramètres
• les composants peuvent dire si leur invariant est vérifiable, et si oui, si des données le satisfont
  
• d'un mode d'exécution pas à pas assez sommaire

  • prévoir un mécanisme permettant de vérifier les pre d'un requis lors de l'appel en mode “solo” - suppose un état du contexte virtuel (non géré actuellement)

• le service termine (il faut pouvoir interrompre le service s'il est “manifestement” en boucle infinie du fait d'une mutation) sans déclencher d'exception
• les services appelés le sont dans le respect de leur pre condition (Exception sinon)
• la post du service est respectée (vérifié à la fin)
• l'invariant du service est respecté (vérifié à chaque état des zones interruptibles du service et à la fin)

• les paramètres d'appel du service (conformes à la pre)
  • se servir des gardes utilisant les paramètres pour partitionner des domaines (créer un jeu de DT pour garde vraie, et un jeu pour garde fausse)
  • version brutale et simple pour obtenir les DT : générer des DT, tester les pre et éliminer les DT qui ne passent pas (pour les ensembles avec un il existe ou un for all)

    • l'état initial du composant (conforme à l'invariant) (et éventuellement à la PRE du service testé
    • se servir des gardes utilisant les états pour partitionner des domaines (créer un jeu de DT pour garde vraie, et un jeu pour garde fausse)
• les réceptions de services (conformes à la post du requis : peut dépendre des entrées, du contexte virtuel …)
  • injecter a partir de bouchons (peuvent utiliser les post des requis pour tester la validité avant l'injection)
    (en fait les données peuvent etre générées conformes aux contraintes : cool!)

mutations cohérentes du LTS : par catégories :

• gardes
• actions élémentaires

modification effectuées :

• substitutions d'opérations à signature compatible - FAIT
• (et de variables à type compatibles ?) et ?

peut on se permettre de modifier le déroulement du LTS et des comms ? Il faudrait le faire de façon a n'introduire ni deadlock, ni boucles infinies. C'est très limitant. et dur a détecter. Plus tard ….

Bankaccount, service transaction supposé unique

utilisation des gardes pour partitionner le domaine

pour la generation de mutation, pourrait on prévoir une annotation à mettre sur les methodes concernées par la mutation (ou à ne pas muter) ?

est il raisonnable de muter le lts (et pas seulement ses actions) ? si oui, quelles mutations seraient pertinentes ?

• scheduler sans delai - FAIT mais non commité
• injecter des données à l'appel ( l'appel est aussi considéré comme un appel sur canal+message donc voir ci dessous)
• en reception de message ( canal+message)

  • modif etat composant - FAIT : getters et setters (uniquement pour le test bien sûr)
  • equals sur comp - FAIT