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

Sandrine-Dominique Gouraud 1 Arnaud Gotlieb 1
1 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Résumé : Le 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.
Complete list of metadatas

https://hal.inria.fr/inria-00000075
Contributor : Christine Solnon <>
Submitted on : Thursday, May 26, 2005 - 11:39:33 AM
Last modification on : Friday, November 16, 2018 - 1:30:33 AM
Long-term archiving on : Thursday, April 1, 2010 - 8:06:07 PM

Files

Identifiers

  • HAL Id : inria-00000075, version 1

Citation

Sandrine-Dominique Gouraud, Arnaud Gotlieb. Utilisation des CHRs pour générer des cas de test fonctionnel pour la Machine Virtuelle Java Card. Premières Journées Francophones de Programmation par Contraintes, CRIL - CNRS FRE 2499, Jun 2005, Lens, pp.383-392. ⟨inria-00000075⟩

Share

Metrics

Record views

166

Files downloads

76