Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java | SpringerLink
Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
  • First Online:
FME 2002:Formal Methods—Getting IT Right (FME 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2391))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. E. Bretagne, A. El Marouani, P. Girard, and J.-L. Lanet. Pacap purse and loyalty specification. Technical Report V 0.4, Gemplus, 2000.

    Google Scholar 

  2. C. Breunesse, B. Jacobs, and J. van den Berg. Specifying and Verifying a Decimal Representation in Java for Smart Cards. In Algebraic Methodology And Software Technology (AMAST’ 02), LNCS. Springer, 2002. To appear.

    Google Scholar 

  3. N. Cataño and M. Huisman. Annotated files Electronic Purse case study, 2001. http://www-sop.inria.fr/lemme/verificard/electronicpurse.

  4. N. Cataño and M. Huisman. A static checker for JML’s assignable clause, 2002. Manuscript.

    Google Scholar 

  5. Differences between Esc/Java and JML, 2000. Comes with JML distribution, in file esc-jml-diffs.txt.

    Google Scholar 

  6. Extended static checking for Java. http://research.compaq.com/SRC/esc/.

  7. ESC/Java specifications for the JavaCard API. http://www.cs.kun.nl/~erikpoll/publications/jc211specs.html.

  8. Gemplus. Applet benchmark kit. http://www.gemplus.com/smart/rd/publications/case-study/.

  9. M. Huisman, B. Jacobs, and J. van den Berg. A Case Study in Class Library Verification: Java’s Vector Class. Software Tools for Technology Transfer, 3/3:332–352, 2001.

    Google Scholar 

  10. The JASS project. http://semantik.informatik.uni-oldenburg.de/~jass/.

  11. G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary Design of JML: a Behavioral Interface Specification Language for Java. Technical Report 98-06, Iowa State University, Department of Computer Science, 2000.

    Google Scholar 

  12. K.R.M. Leino, G. Nelson, and J.B. Saxe. ESC/Java user’s manual. Technical Report SRC 2000-002, Compaq System Research Center, 2000.

    Google Scholar 

  13. The LOOP project. http://www.cs.kun.nl/~bart/LOOP/.

  14. H. Meijer and E. Poll. Towards a Full Formal Specification of the Java Card API. In I. Attali and T. Jensen, editors, Smart Card Programming and Security (E-smart 2001), number 2140 in LNCS, pages 165–178. Springer, 2001.

    Chapter  Google Scholar 

  15. B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.

    Google Scholar 

  16. J. Meyer and A. Poetzsch-Heffter. An architecture of interactive program provers. In S. Graf and M. Schwartzbach, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000), number 1785 in LNCS, pages 63–77. Springer, 2000.

    Chapter  Google Scholar 

  17. Sun Microsystems, Inc. Java Card 2.1. Platform Application Programming Interface (API) Specification. http://java.sun.com/products/javacard/htmldoc/.

  18. Sun Microsystems, Inc. JavaCard Technology. http://java.sun.com/products/javacard/.

  19. K. Trentelman and M. Huisman. Extending JML Specifications with Temporal Logic. In Algebraic Methodology And Software Technology (AMAST’ 02), LNCS. Springer, 2002. To appear.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, Sophia-Antipolis, France

    Néstor Cataño & Marieke Huisman

Authors
  1. Néstor Cataño
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marieke Huisman
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Information Technology, Uppsala University, P.O. Box 337, 751 05, Uppsala, Sweden

    Lars-Henrik Eriksson

  2. Software Verification Research Centre, The University of Queensland, Queensland, 4072, Australia

    Peter Alexander Lindsay

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cataño, N., Huisman, M. (2002). Formal Specification and Static Checking of Gemplus’ Electronic Purse Using ESC/Java. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_16

Download citation

  • DOI: https://doi.org/10.1007/3-540-45614-7_16

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43928-8

  • Online ISBN: 978-3-540-45614-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation