Model-Based Test Case Generation for Smart Cards1 1Support by the BMBF (project EMPRESS) is gratefully acknowledged.

Testing denotes a set of activities that aim at discovering discrepancies between actual and intended behaviors of a system. Often, the intended behavior is known only implicitly, which renders the process of testing unstructured, unmotivated in its details, and barely reproducible. The use of explicit and executable models to describe the intended behavior promises to solve these problems. We use an industrial case study — a smart card application — to present a method for automatically generating test cases from such explicit models. The test cases are used both to validate the model and verify the actual card.