Abstract
This paper presents a systematic approach to developing Java Card applets and/or formal specifications for then, starting from descriptions in the form of finite state machines. The formal specifications are written in the specification language JML, and can be checked against Java Card source code using the static checker ESC/Java.
The original version of this chapter was revised: The copyright line was incorrect. This has been corrected. The Erratum to this chapter is available at DOI: 10.1007/978-0-387-35691-4_52
Chapter PDF
References
Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. (1998). Extended Static Checking. Technical Report 159, Compaq Systems Research Center.
Leavens, G. T., Baker, A. L., and Ruby, C. (1999). JML: A notation for detailed design. In Kilov, H., Rumpe, B., and Harvey, W., editors, Behavioral Specifications for Businesses and Systems,pages 175-188. Kluwer Academic Publishers.
Marlet, R. and Métayer, D. L. (2001). Security properties and Java Card specificities to be studied in the SecSafe project. Technical Report SECSAFE-TL-006, Trusted Logic.
Mostowski, W. (2002). Rigorous development of.JavaCard applications. In Clarke, T., Evans, A., and Lano, K., editors, Proc. Fourth Workshop on Rigorous Object-Oriented Methods, London.
Pettersson, P. and Larsen., K. G. (2000). UPPAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70: 40 - 44.
Poll, E., van den Berg, J., and Jacobs, B. (2000). Specification of the Java Card API in JML. In Domingo-Ferrer, J., Chan, D., and Watson, A., editors, Fourth Smart Card Research and Advanced Application Conference (CARDIS 2000),pages 135154. Kluwer.
Van den Berg, J. and Jacobs, B. (2001). The LOOP compiler for Java and JML. In Margaria, T. and Yi, W., editors, Tools and Algorithms for the Construction and Analysis of Software (TACAS), volume 2031 of LNCS, pages 299-312. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Hubbers, E., Oostdijk, M., Poll, E. (2003). From Finite State Machines to Provably Correct Java Card Applets. In: Gritzalis, D., De Capitani di Vimercati, S., Samarati, P., Katsikas, S. (eds) Security and Privacy in the Age of Uncertainty. SEC 2003. IFIP — The International Federation for Information Processing, vol 122. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35691-4_47
Download citation
DOI: https://doi.org/10.1007/978-0-387-35691-4_47
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4757-6489-5
Online ISBN: 978-0-387-35691-4
eBook Packages: Springer Book Archive