Abstract
Usually, testing smart card software is carried-out by specialized engineers in a proprietary language. Testing represents generally half of smart card development effort. With the increasing use of semi-formal and formal modeling languages, such as UML, and the emergence of automatic test generators in the industry, we have studied a way to adapt these techniques for smart card. In this article, we present an automatic test generator, named AGATHA, and its architecture, which can handle UML specifications. Then, we suggest a way to model (U)SIM smart card functionalities in UML. We use the test generator on our (U)SIM smart card UML models and automatically produce our first test cases.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abrial, J.R.: The B-Book, Assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Behnia, S., Waeselynck, H.: Test criteria definition for B models. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 509–529. Springer, Heidelberg (1999)
Bernard, E., Legeard, B., Luck, X., Peureux, F.: Generation of test sequences from formal specifications: GSM 11.11 standard case-study. The Journal of Software Practice and Experience 34(10), 915–948 (2004)
Bigot, C., Faivre, A., Gallois, J.P., Lapitre, A., Lugato, D., Pierron, J.Y., Rapin, N.: Automatic test generation with AGATHA, TACAS, April 7-11 (2003)
Bouquet, F., Peureux, F.: Generation of functional test sequences from B formal specifications – Presentation and industrial case-study. In: Procs. of the 16th International Conference on Automated Software Engineering (ASE 2001), San Diego (USA), pp. 377–381 (November 2003)
Bouquet, F., Legeard, B., Peureux, F., Torreborre, E.: Mastering Test Generation from Smartcard Software Formal Models. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 70–85. Springer, Heidelberg (2005)
Carre, O., Martin, H., Vandewalle, J.J.: A semi formal model of Java Card 2.1 in UML. In: 1st Gemplus Developer Conference, Paris, France, June 21-22 (1999)
Clarke, D., Jéron, T., Rusu, V., Zinovieva, E.: Automated test and oracle generation for smart-card applications. In: Attali, S., Jensen, T. (eds.) E-smart 2001. LNCS, vol. 2140, pp. 58–70. Springer, Heidelberg (2001)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Cheking. The MIT press, Cambridge (1999)
Clarke, L.A.: A System to Generate Test Data and Symbolically Execute Programs. IEEE Transactions on Software Engineering SE-4(3), 178–187 (1976)
Dick, J., Faivre, A.: Automating the generation and sequencing of test cases from modelbased specifications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993)
European Telecommunications Standards Institute, F-06921 Sophia Antipolis (France), GSM 11.11 v7.2.0 Technical Specification (1999)
European Telecommunications Standards Institute, F-06921 Sophia Antipolis (France), GSM 11.17 v8.1.0 Technical Specification (1999)
Faivre, A., Gaston, C.: Test generation methodology based on symbolic execution for the Common Criteria higher levels. In: MoDeVa workshop, Montego Bay (Jamaica) (October 2005)
Fernandez, J.C., Jard, C., Jéron, T., Viho, C.: Using on the fly verification techniques for the generation of test suites. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 145–150. Springer, Heidelberg (1996)
Gallois, J.P., Lanusse, A.: Le test structurel pour la vérification de spécifications de systèmes industriels. Génie logiciel (46), 145–150 (1997)
Gallois, J.P., Lapitre, A., Lé, P.: Analyse de spécifications industrielles et génération automatique de tests. In: ICSSEA 1999, CNAM-Paris, France, décembre 8-10 (1999)
Hennessy, M., Lin, H.: Symbolic bisimulations. Theorical Computer Science, vol. 138, pp. 353–389. Elsevier, Amsterdam (1995)
Hierons, R.: Testing from Z specification. The journal of Software Testing, Verification and Reliability 7, 19–33 (1997)
International Union of Telecommunications, Langage de programmation – Langage de Description et de Spécification du CCITT – Norme 34, Recommandation UIT T Z.100 (March 1993)
Ishisone, M., Sawada, T.: Brute: brute force rewriting engine, GAIST cafeobj (January 2001), http://www.thetatheta.ro/
Jeannet, B., Jéron, T., Rusu, V., Zinovieva, E.: Symbolic Test Selection Based on Approximate Analysis. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 349–364. Springer, Heidelberg (2005)
Kelly, W., Maslov, V., Pugh, W., Rosser, E., Shpeisman, T., Wonnacott, D.: The Omega Library version 1.1.0, University of Maryland (November 1996), http://www.cs.umd.edu/projects/omega
King, J.C.: Symbolic Execution and Program Testing. communications de l’ACM 19(7), 385–394 (1976)
Lapitre, A.: Procédure de réduction pour les systèmes à base d’automates communicants: formalisation et mise en oeuvre, Phd Thesis, University of Paris XI, in collaboration with the CEA (December 2002)
LEIRIOS tool, http://www.leirios.com/index.php
Lin, H.: Symbolic Transition Graph with Assignment. In: CONCUR 1996. LNCS, Springer, Heidelberg (August 1996)
Lugato, D., Bigot, C., Valot, Y.: Validation and automatic test generation on UML models: the AGATHA approach. STTT (Software Tools for Technology Transfer) 5(2), 124–139 (2004)
Martin, H., du Bousquet, L.: Automatic test generation for Java-Card applets. In: Java card Workshop, Cannes (France) (September 2000)
OMG, Unified Modelling Language 2.0, OMG, Rapport formel/2003-04-01 (January 2003)
Philipps, J., Pretschner, A., Slotosch, O., Aiglestorfer, E., Kriebel, S., Scholl, K.: Modelbased test case generation for smartcards. In: procs. of the 8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003), Trondheim (Norway). ENTCS, vol. 80 (June 2003)
Pierron, J.Y., Gallois, J.-P., Fievet, E., Lapitre, A., Lugato, D.: Validation de systèmes industriels par le test symbolique sur spécification STATEMATE. In: ICSSEA 2000, CNAMParis, France, December 5-8 (2000)
Pierron, J.Y.: Définition de critères de sélection de tests fonctionnels pour la validation des systèmes électroniques embarqués, Phd Thesis, University of Evry, France, in collaboration with the CEA and PSA (April 2003)
Rapin, N.: Validation de spécification à base d’automates par des techniques de dépliages et d’exécution symbolique, Phd Thesis, University of Evry (France), in collaboration with the CEA and Ligeron S.A. (July 2004)
Wolper, P., Godefroid, P.: Partial-Order Methods for Temporal Verification. In: Procs. of CONCNUR 1993, Hildesheim (Belgium), pp. 233–246 August 1993)
Yovine, S.: Kronos: A verification tool for real time systems. Springer International Journal of Software Tools for Technology Transfer 1(1/2) (August 1993)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 IFIP International Federation for Information Processing
About this paper
Cite this paper
Bigot, C., Faivre, A., Gaston, C., Simon, J. (2006). Automatic Test Generation on a (U)SIM Smart Card. In: Domingo-Ferrer, J., Posegga, J., Schreckling, D. (eds) Smart Card Research and Advanced Applications. CARDIS 2006. Lecture Notes in Computer Science, vol 3928. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11733447_25
Download citation
DOI: https://doi.org/10.1007/11733447_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33311-1
Online ISBN: 978-3-540-33312-8
eBook Packages: Computer ScienceComputer Science (R0)