Utilisation des CHRs pour générer des cas de test fonctionnel pour la Machine Virtuelle Java Card

http://www710.univ-lyon1.fr/~csolnonLe test fonctionnel basé sur une spécification formelle consiste à dériver des cas de test à partir d'un modèle formel pour détecter des fautes dans une implémentation. Dans nos travaux, nous étudions l'utilisation des Constraint Handling Rules (CHRs) pour automatiser la génération de cas de test fonctionnel basée sur un modèle formel. Notre étude de cas est un modèle de la Machine Virtuelle Java Card (JCVM) écrit dans un sous ensemble du langage Coq. Dans cet article, nous définissons une traduction automatique de ce modèle sous forme de règles CHR dans le but de générer des cas de test pour la JCVM. Le point clé de notre approche réside dans l'utilisation des deep guards pour modéliser fidèlement la sémantique de notre modèle formel. Ensuite, nous proposons une approche globale pour la génération de cas de test fonctionnel basée sur les CHRs qui peut être appliquée à d'autres modèles formels