Using CHRs to generate functional test cases for the Java Card Virtual Machine

Sandrine-Dominique Gouraud (1) , Arnaud Gotlieb (1)

1 Lande - Logiciel : ANalyse et DEveloppement

Functional testing based on a formal specification consists in deriving test cases from a formal model to detect faults within an implementation. In our work, we investigate the use of Constraint Handling Rules (CHRs) to automate functional test cases generation based on a formal model. Our case study is a model of the Java Card Virtual Machine (JCVM) specification written in a subset of the Coq language. In this paper we define an automated translation from this model into CHRs in order to generate test cases for the JCVM. We also propose several test purposes based on rewriting rules coverage and automatic non-conformity detection. The key point of our approach resides in the use of deep guards to model faithfully the semantic of our formal model of the JCVM. Finally, we propose an overall functional test case generation approach based on CHRs that could be applied to other formal models / 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.

Mots clés: Test case generation; functional testing; constraint solving; rewriting rules; Constraint Handling Rules (CHR); Jakarta Specification Language (JSL); test fonctionnel; résolution de contraintes; règles de réécriture; Machine Virtuelle Java Card (JCVM); Java Card Virtual Machine (JCVM) :; Génération de cas de test

Domaines: Multimédia [cs.MM]; Langage de programmation [cs.PL]

Sandrine-Dominique Gouraud, Arnaud Gotlieb. Using CHRs to generate functional test cases for the Java Card Virtual Machine. [Research Report] PI 1725, 2005. ⟨inria-00000114⟩