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

Néstor Cataño; Marieke Huisman

doi:10.1007/3-540-45614-7_16

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 proceeding › Conference contribution › Academic › peer-review

30 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 language	English
Title of host publication	FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings
Editors	Lars-Henrik Eriksson, Peter A. Lindsay
Publisher	Springer
Pages	272-289
Number of pages	18
DOIs	https://doi.org/10.1007/3-540-45614-7_16
Publication status	Published - 2002
Externally published	Yes
Event	11th International Symposium of Formal Methods Europe, FME 2002: Formal Methods - Getting IT Right - Copenhagen, Denmark Duration: 22 Jul 2002 → 24 Jul 2002 Conference number: 11

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2391

Conference

Conference	11th International Symposium of Formal Methods Europe, FME 2002
Abbreviated title	FME
Country/Territory	Denmark
City	Copenhagen
Period	22/07/02 → 24/07/02

Access to Document

10.1007/3-540-45614-7_16

Cite this

Cataño, N., & Huisman, M. (2002). Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. In L.-H. Eriksson, & P. A. Lindsay (Eds.), FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings (pp. 272-289). (Lecture Notes in Computer Science; Vol. 2391). Springer. https://doi.org/10.1007/3-540-45614-7_16

Cataño, Néstor ; Huisman, Marieke. / Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings. editor / Lars-Henrik Eriksson ; Peter A. Lindsay. Springer, 2002. pp. 272-289 (Lecture Notes in Computer Science).

@inproceedings{372144f507484698970c398d622dbb35,

title = "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.",

author = "N{\'e}stor Cata{\~n}o and Marieke Huisman",

year = "2002",

doi = "10.1007/3-540-45614-7_16",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "272--289",

editor = "Lars-Henrik Eriksson and Lindsay, {Peter A.}",

booktitle = "FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings",

address = "Germany",

note = "11th International Symposium of Formal Methods Europe, FME 2002 : Formal Methods - Getting IT Right, FME ; Conference date: 22-07-2002 Through 24-07-2002",

}

Cataño, N & Huisman, M 2002, Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. in L-H Eriksson & PA Lindsay (eds), FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2391, Springer, pp. 272-289, 11th International Symposium of Formal Methods Europe, FME 2002, Copenhagen, Denmark, 22/07/02. https://doi.org/10.1007/3-540-45614-7_16

Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. / Cataño, Néstor; Huisman, Marieke.
FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings. ed. / Lars-Henrik Eriksson; Peter A. Lindsay. Springer, 2002. p. 272-289 (Lecture Notes in Computer Science; Vol. 2391).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

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

AU - Cataño, Néstor

AU - Huisman, Marieke

N1 - Conference code: 11

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

U2 - 10.1007/3-540-45614-7_16

DO - 10.1007/3-540-45614-7_16

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 272

EP - 289

BT - FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings

A2 - Eriksson, Lars-Henrik

A2 - Lindsay, Peter A.

PB - Springer

T2 - 11th International Symposium of Formal Methods Europe, FME 2002

Y2 - 22 July 2002 through 24 July 2002

ER -

Cataño N, Huisman M. Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. In Eriksson LH, Lindsay PA, editors, FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings. Springer. 2002. p. 272-289. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45614-7_16

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this