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
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : 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.
Complete list of metadatas

Cited literature [17 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000114
Contributor : Anne Jaigu <>
Submitted on : Friday, June 17, 2005 - 10:43:32 AM
Last modification on : Friday, November 16, 2018 - 1:25:07 AM
Long-term archiving on : Thursday, April 1, 2010 - 9:42:46 PM

Identifiers

  • HAL Id : inria-00000114, version 1

Citation

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⟩

Share

Metrics

Record views

379

Files downloads

348