Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java

Néstor Cataño, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

25 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationFME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings
EditorsLars-Henrik Eriksson, Peter A. Lindsay
PublisherSpringer Singapore
Pages272-289
Number of pages18
DOIs
Publication statusPublished - 2002
Externally publishedYes
EventFormal Methods - Getting IT Right, FME 2002: 11th International Symposium of Formal Methods Europe - Copenhagen, Denmark
Duration: 22 Jul 200224 Jul 2002
Conference number: 11

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume2391

Conference

ConferenceFormal Methods - Getting IT Right, FME 2002
Abbreviated titleFME
CountryDenmark
CityCopenhagen
Period22/07/0224/07/02

Fingerprint Dive into the research topics of 'Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java'. Together they form a unique fingerprint.

Cite this