Abstract
The Java dialect Java Card for programming smartcards contains some features which do not exist in Java. Java Card distinguishes persistent and transient data (data stored in EEPROM and RAM, respectively). Because power to a smartcard can suddenly be interrupted by a so-called card tear, by someone removing the smartcard from the reader, Java Card provides a notion of transaction to ensure that updates of multiple fields in persistent memory can be performed atomically. This paper describes a way to reason about these Java Card specific language features.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Beckert, B., Mostowski, W.: A program logic for handling Java Card’s transaction mechanism. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 246–260. Springer, Heidelberg (2003)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pp. 73–89. Elsevier, Amsterdam (2003)
Jacobs, B., Poll, E.: Java program verification at Nijmegen: Developments and perspective. Technical Report NIII-R0318, Dept. of Computer Science, Univiversity of Nijmegen (2003)
Hartel, P.H., de Jong Frz, E.K.: A programming and a modelling perspective on the evaluation of Java card implementations. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 52–72. Springer, Heidelberg (2001)
Poll, E., Hartel, P., de Jong, E.: A Java reference model of transacted memory for smart cards. In: Fifth Smart Card Research and Advanced Application Conference (CARDIS 2002), pp. 75–86. USENIX (2002)
Chen, Z.: Java Card Technology for Smart Cards. The Java Series. Addison-Wesley, Reading (2000)
Sun: Java Card 2.1 Runtime Environment (JCRE) Specification. Sun Micro systems Inc., Palo Alto, California (1999), http://java.sun.com/products/javacard/
Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)
Oestreicher, M.: Transactions in Java Card. In: 15th Annual Computer Security Applications Conf. (ACSAC), Phoenix, Arizona, pp. 291–298. IEEE Comput. Soc., Los Alamitos (1999), http://www.acsac.org/1999/abstracts/thu-b-1500-marcus.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hubbers, E., Poll, E. (2004). Reasoning about Card Tears and Transactions in Java Card. In: Wermelinger, M., Margaria-Steffen, T. (eds) Fundamental Approaches to Software Engineering. FASE 2004. Lecture Notes in Computer Science, vol 2984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24721-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-24721-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21305-5
Online ISBN: 978-3-540-24721-0
eBook Packages: Springer Book Archive