Formal methods for smart cards: an experience report

Cees-Bart Breunesse, Néstor Cataño, Marieke Huisman, Bart Jacobs

Research output: Contribution to journalArticleAcademicpeer-review

24 Citations (Scopus)
13 Downloads (Pure)


This paper presents a case study in the formal specification and verification of a smart card application. The application is an electronic purse implementation, developed by the smart card producer Gemplus as a test case for formal methods for smart cards. It has been annotated (by the authors) with specifications using the Java Modeling Language (JML), a language designed to specify the functional behavior of Java classes. The reason for using JML as a specification language is that several tools are available to check (parts of) the specification w.r.t. an implementation. These tools vary in their level of automation and in the level of correctness they ensure. Several of these tools have been used for the Gemplus case study. We discuss how the usage of these different tools is complementary: large parts of the specification can be checked automatically, while more precise verification methods can be used for the more intricate parts of the specification and implementation. We believe that having such a range of tools available for a single specification language is an important step towards the acceptance of formal methods in industry.
Original languageEnglish
Pages (from-to)53-80
Number of pages28
JournalScience of computer programming
Issue number1-3
Publication statusPublished - 2005
Externally publishedYes


Dive into the research topics of 'Formal methods for smart cards: an experience report'. Together they form a unique fingerprint.

Cite this