Abstract
Automated functional testing consists in deriving test cases from the specification model of a program to detect faults within an implementation. In our work, we investigate using Constraint Handling Rules (CHRs) to automate the test cases generation process of functional testing. Our case study is a formal model of the Java Card Virtual Machine (JCVM) written in a sub-language of the Coq proof assistant. In this paper we define an automated translation from this formal model into CHRs and propose to generate test cases for each bytecode definition of the JCVM. The originality of our approach resides in the use of CHRs to faithfully model the formally specified operational semantics of the JCVM. The approach has been implemented in Eclipse Prolog and a full set of test cases have been generated for testing the JCVM.
This work is supported by theRéseau National des Technologies Logicielles as part of theCASTLES project (www-sop.inria.fr/everest/projects/castles/). This project aims at defining a certification environment for the JavaCard platform. The project involves two academic partners: the Everest and Lande teams of INRIA and two industrial partners: Oberthur Card Systems and Alliance Qualité Logicielle.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bernot, G., Gaudel, M.C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Software Engineering Journal 6, 387–405 (1991)
Bernard, E., Legeard, B., Luck, X., Peureux, F.: Generation of test sequences from formal specifications: GSM 11-11 standard case study. International Journal of Software Practice and Experience 34, 915–948 (2004)
Grieskamp, W., Gurevich, Y., Schulte, W., Veanes, M.: Generating finite state machines from abstract state machines. In: ISSTA 2002: Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, pp. 112–122. ACM Press, New York (2002)
Barthe, G., Dufay, G., Huisman, M., Sousa, S.: Jakarta: A toolset for reasoning about javaCard. In: Attali, I., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 2–18. Springer, Heidelberg (2001)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 302–319. Springer, Heidelberg (2001)
Brisset, P., Sakkout, H., Fruhwirth, T., Gervet, C.: Harvey, W., et al.: ECLiPSe Constraint Library Manual. International Computers Limited and Imperial College London, UK, Release 5.8 (2005)
de Sousa, S.M.: Outils et techniques pour la vérification formelle de la plate-forme JavaCard. PhD thesis, Université de Nice (2003)
Frühwirth, T.: Theory and Practice of Constraint Handling Rules. Logic Programming 37 (1998) In: Stuckey, P., Marriott, K. (eds.) Special Issue on Constraint Logic Programming
Frühwirth, T., Abdennadher, S.: Essentials of Constraint Programming. Cognitive Technologies. Springer, Heidelberg (2003) ISBN 3-540-67623-6
Duck, G., Stuckey, P., de la Banda, M.G., Holzbaur, C.: Extending arbitrary solvers with constraint handling rules. In: Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming (PPDP 2003), pp. 79–90 (2003)
Schulte, C.: Programming deep concurrent constraint combinators. In: Pontelli, E., Santos Costa, V. (eds.) PADL 2000. LNCS, vol. 1753, pp. 215–229. Springer, Heidelberg (2000)
Podelski, A., Smolka, G.: Situated Simplification. In: Montanari, U., Rossi, F. (eds.) CP 1995. LNCS, vol. 976, pp. 328–344. Springer, Heidelberg (1995)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., de Sousa, S.M., Yu, S.W.: Formalization of the JavaCard Virtual Machine in Coq. In: Drossopoulou, S., et al. (eds.) Proceedings of FTfJP 2000 (ECOOP Workshop on Formal Techniques for Java Programs), pp. 50–56 (2000)
Dufay, G.: Vérification formelle de la plate-forme Java Card. PhD thesis, Université de Nice-Sophia Antipolis (2003)
Gouraud, S.D., Denise, A., Gaudel, M.C., Marre, B.: A New Way of Automating Statistical Testing Methods. In: Sixteenth IEEE International Conference on Automated Software Engineering (ASE), pp. 5–12 (2001)
Flajolet, P., Zimmermann, P., Van Cutsem, B.: A calculus for the random generation of labelled combinatorial structures. Theoretical Computer Science 132, 1–35 (1994)
Denise, A., Gaudel, M.C., Gouraud, S.D.: A Generic Method for Statistical Testing. In: Fifteenth IEEE International Symposium on Software Reliability Engineering, pp. 25–34 (2004)
Gotlieb, A., Botella, B., Rueher, M.: A CLP Framework for Computing Structural Test Data. In: Oliveira, A.L. (ed.) ICGI 2000. LNCS, vol. 1891, pp. 399–413. Springer, Heidelberg (2000)
Pretschner, A., Lötzbeyer, H.: Model Based Testing with Constraint Logic Programming: First Results and Challenges. In: Proceedings 2nd ICSE Intl. Workshop on Automated Program Analysis, Testing and Verification (2001)
Lötzbeyer, H., Pretschner, A.: AutoFocus on Constraint Logic Programming. In: Proceedings of (Constraint) Logic Programming and Software Engineering, LPSE 2000 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gouraud, SD., Gotlieb, A. (2005). Using CHRs to Generate Functional Test Cases for the Java Card Virtual Machine. In: Van Hentenryck, P. (eds) Practical Aspects of Declarative Languages. PADL 2006. Lecture Notes in Computer Science, vol 3819. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11603023_1
Download citation
DOI: https://doi.org/10.1007/11603023_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30947-5
Online ISBN: 978-3-540-31685-5
eBook Packages: Computer ScienceComputer Science (R0)