Abstract
In this paper we extend a program logic for verifying JAVA CARD applications by introducing a “throughout” operator that allows us to prove “strong” invariants. Strong invariants can be used to ensure “rip out” properties of JAVACARD programs (properties that are to be maintained in case of unexpected termination of the program). Along with introducing the “throughout” operator, we show how to handle the JAVACARD transaction mechanism (and, thus, conditional assignments) in our logic. We present sequent calculus rules for the extended logic.
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
W. Ahrendt, T. Baar, B. Beckert, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, and P. H. Schmitt. The KeY system: Integrating object-oriented design and formal methods. In R.-D. Kutsche and H. Weber, editors, Proceedings, Fundamental Approaches to Software Engineering (FASE), Grenoble, France, LNCS 2306, pages 327–330. Springer, 2002.
B. Beckert. A dynamic logic for the formal verification of JAVACARD programs. In I. Attali and T. Jensen, editors, Revised Papers, JAVA on Smart Cards: Programming and Security, Cannes, France, LNCS 2041, pages 6–24. Springer, 2001.
B. Beckert and B. Sasse. Handling JAVA’s abrupt termination in a sequent calculus for Dynamic Logic. In B. Beckert, R. France, R. Hähnle, and B. Jacobs, editors, Proceedings, IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development, Siena, Italy, pages 5–14. TR DII 07/01, Dipartimento di Ingegneria dell’Informazione, Università degli Studi di Siena, 2001.
B. Beckert and S. Schlager. A sequent calculus for first-order dynamic logic with trace modalities. In R. Gorè, A. Leitsch, and T. Nipkow, editors, Proceedings, International Joint Conference on Automated Reasoning, Siena, Italy, LNCS 2083, pages 626–641. Springer, 2001.
J. C. Bradfield, J. K. Filipe, and P. Stevens. Enriching OCL using observational mu-calculus. In R.-D. Kutsche and H. Weber, editors, Proceedings, Fundamental Approaches to Software Engineering (FASE), Grenoble, France, LNCS2306, pages 203–217. Springer, 2002.
Z. Chen. JAVACARD Technology for Smart Cards. Addison Wesley, 2000.
D. Harel. Dynamic Logic. In D. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic. Reidel, 1984.
D. Harel, D. Kozen, and J. Tiuryn. Dynamic Logic. MIT Press, 2000.
D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 14, pages 89–133. Elsevier, 1990.
W. Mostowski. Rigorous development of JAVACARD applications. In T. Clarke, A. Evans, and K. Lano, editors, Proc. Fourth Workshop on Rigorous Object-Oriented Methods, London, 2002. http://www.cs.chalmers.se/~woj/papers/room2002.ps.gz.
V. R. Pratt. Semantical considerations on Floyd-Hoare logic. In Proceedings, 18th Annual IEEE Symposium on Foundation of Computer Science, 1977.
Sun Microsystems, Inc. JAVACARD 2.2 Application Programming Interface, 2002.
Sun Microsystems, Inc. JAVACARD 2.2 Runtime Environment Specification, 2002.
Sun Microsystems, Inc. JAVACARD 2.2 Virtual Machine Specification, 2002.
K. Trentelman and M. Huisman. Extending JML specifications with temporal logic. In Algebraic Methodology And Software Technology (AMAST’ 02), LNCS 2422, pages 334–348. Springer-Verlag, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B., Mostowski, W. (2003). A Program Logic for Handling Java Card’s Transaction Mechanism. In: Pezzè, M. (eds) Fundamental Approaches to Software Engineering. FASE 2003. Lecture Notes in Computer Science, vol 2621. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36578-8_18
Download citation
DOI: https://doi.org/10.1007/3-540-36578-8_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00899-6
Online ISBN: 978-3-540-36578-5
eBook Packages: Springer Book Archive