Formal specification and static checking of Gemplus’ electronic purse using ESC/Java

Abstract

This paper presents a case study in formal specification of smart card programs, using ESC/Java. It discusses an electronic purse application, provided by Gemplus, that we have annotated with functional specifications (i.e. pre- and postconditions, modifies clauses and class invariants), that are as detailed as possible. The specification is based on the informal documentation of the application. Using ESC/Java, the implementation has been checked w.r.t. the specification. This revealed several errors or possibilities for improvement in the source code (e.g. removing unnecessary tests). Our paper shows that a relatively lightweight use of formal specification techniques can already have a serious impact on the quality of a program and its documentation. Furthermore, we also present some ideas on how ESC/Java could be further improved, both w.r.t. specification and verification.