Abstract
In this paper, we define a program logic (an instance of Dynamic Logic) for formalising properties of Java Card programs, and we give a sequent calculus for formally verifying such properties. The purpose of this work is to provide a framework for software verification that can be integrated into real-world software development processes.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, and P. H. Schmitt. The KeY approach: Integrating object oriented design and formal verification. In M. Ojeda-Aciego, I. P. de Guzman, G. Brewka, and L. M. Pereira, editors, Proceedings, Logics in Artificial Intelligence (JELIA), Malaga, Spain, LNCS 1919. Springer, 2000.
J. Alves-Foss, editor. Formal Syntax and Semantics ofJava. LNCS 1523. Springer, 1999.
K. R. Apt. Ten years of Hoare logic: A survey-part I. ACM Transactions on Programming Languages and Systems, 1981.
T. Baar. Experiences with the UML/OCL-approach to precise software modeling: A report from practice. Available at i12www.ira.uka.de/~key, 2000.
E. Börger and W. Schulte. A programmer friendly modular definition of the semantics of Java. In Alves-Foss [2], pages 353–404.
C. Calcagno, S. Ishtiaq, and P. W. O’Hearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. In Proceedings, International Conference on Principles and Practice of De clarative Programming, Montreal, Canada. ACM, 2000.
E. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys, 28(4):626–643, 1996.
D. L. Dill and J. Rushby. Acceptance of formal methods: Lessons from hardware design. IEEE Computer, 29(4):23–24, 1996. Part of: Hossein Saiedian (ed.). An Invitation to Formal Methods. Pages 16-30.
J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison Wesley, second edition, 2000.
M. G. Hinchey and J. P. Bowen, editors. Applications ofF ormal Methods. Prentice Hall, 1995.
M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In Proceedings, Fundamental Approaches to Software Engineering (FASE), Berlin, Germany, LNCS 1783. Springer, 2000.
D. Hutter, B. Langenstein, C. Sengler, J. H. Siekmann, and W. Stephan. Deduction in the Verification Support Environment (VSE). In M.-C. Gaudel and J. Woodcock, editors, Proceedings, International Symposium ofF ormal Methods Europe (FME), Oxford, UK, LNCS 1051. Springer, 1996.
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes (preliminary report). In Proceedings, Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329–340. ACM Press, 1998.
D. Kozen and J. Tiuryn. Logic of programs. In J. van Leeuwen, editor, Handbook ofThe oretical Computer Science, volume B: Formal Models and Semantics, chapter 14, pages 789–840. Elsevier, Amsterdam, 1990.
J. Martin and J. J. Odell. Object-Oriented Methods: A Foundation, UML Edition. Prentice-Hall, 1997. 24 B. Beckert
T. Nipkow and D. von Oheimb. Machine-checking the Java specification: Proving type safety. In Alves-Foss [2], pages 119–156.
T. Nipkow, D. von Oheimb, and C. Pusch. µJava: Embedding a programming language in a theorem prover. In F. L. Bauer and R. Steinbrüggen, editors, Foundations ofSe cure Computation. IOS Press, 2000. To appear.
Object Management Group, Inc., Framingham/MA, USA, www.omg.org. OMG Unified Modeling Language Specification, Version 1.3, June 1999.
A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In S. D. Swierstra, editor, Proceedings, Programming Languages and Systems (ESOP), Amsterdam, The Netherlands, LNCS 1576, pages 162–176. Springer, 1999.
W. Reif.The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report, LNCS 1009. Springer, 1995.
D. von Oheimb. Axiomatic semantics for Javaight. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, Proceedings, Formal Techniques for Java Programs, Workshop at ECOOP’00, Cannes, France, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beckert, B. (2001). A Dynamic Logic for the Formal Verification ofJava Card Programs. In: Attali, I., Jensen, T. (eds) Java on Smart Cards:Programming and Security. JavaCard 2000. Lecture Notes in Computer Science, vol 2041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45165-X_2
Download citation
DOI: https://doi.org/10.1007/3-540-45165-X_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42167-2
Online ISBN: 978-3-540-45165-5
eBook Packages: Springer Book Archive