====== Kmelia - Le test ====== [[photo tableau]] ====Exemple support ==== * au niveau modele et non meta ==== Originalité ==== * 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) ==== Construction de cas de test et paramétrage ==== === Caractéristiques de l'exécution du test (trouver un nom pour ce machin !) === * états * traces * assertions * exceptions * résultat (retour) === Verdict se basant sur le test === * pass/fail/irrelevant * responsabilité ( programme, source de donnée) * confiance (exception lourde (div/0), assertions, boucle inf ...) === Utilisation variable de l'observation de l'exécution du test selon l'objectif === * 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 ==== Particularités vis a vis de Baudry/traon ==== : 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) ====Mutation ==== * 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 ====== Nouvelle Version : mutations du modèle et pas du java ====== voir, pour référence, la [[costo:plugins:kml2java|page sur la génération de code java]] Attention : gros brouillon en vue ... ===== que teste-t'on ? ===== * 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 ===== De quoi dispose t'on : ===== * 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) ===== test passé si : ===== * 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) =====Que sont les données de test, comment les générer (et les injecter) : ===== * 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 sur le modèle===== 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 .... ====== Vieille version ====== ===== Sujet ===== Bankaccount, service transaction supposé unique ===== Protocole simple ===== utilisation des gardes pour partitionner le domaine ==== Mutations ==== 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 ? ===== A ajouter à la génération ===== * 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