Automated test and oracle generation for Smart-Card applications. 
In International Conference on Research in Smart Cards (e-Smart'01), 
pp. 58-70, 2001. LNCS 2140.

Abstract:

We present work we are engaged in to develop symbolic test generation
techniques and apply those techniques to the testing of smart card
applications.

Beginning with a system specification anda test purpose expressed
as symbolic labelled-transition-systems, we automatically derive tests
to check conformance of an implementation to the behaviors of the 
specification selected by the test purpose.

We present an example taken from a case-study we are developing based on
the application of these techniques to the CEPS e-purse specifications.