Abstract
So far in this book no specific Java Card examples have been discussed, apart from very simple transactions related examples in Chapter 9. In this chapter we are going to discuss how the KeY system is used to verify real world Java Card programs. The basis and running example for this chapter is the demonstrative Java Card electronic purse application Demoney provided by
Trusted Logic S.A. The purpose of this chapter is not to present full specifications for Demoney and a thorough verification procedure, or give a tutorial on using the KeY system verification facilities (\(\Rightarrow\) Chap. 10). Rather, we will discuss general problems associated with Java Card verification attempts: provide advice on what to specify about Java Card applets, how to specify it using different specification languages, and give the reader hints necessary to perform efficient verification of his or her own Java Card applets. Verifications that we are going to discuss were performed on an absolutely unmodified source code of Demoney, thus, the context of this chapter is slightly different from the rest of the book—we do not consider the use of formal methods during the development process, instead we show how one can verify preexisting, legacy Java Card code, in other words, perform post-hoc verification. We also assume that, to a certain extent, the reader is familiar with Java Card technology, described by Chen [2000] (\(\Rightarrow\) Chap. 9).
In the next section we present the Demoney application in more detail, in Section 14.3 we discuss different specification techniques and languages available in the KeY system, their advantages and disadvantages in the context of Demoney verification. Section 14.4 discusses modular verification and the use of method contracts in proofs, which is necessary to make the verification process scalable. Then in Section 14.5 different properties related to Java Card applets are presented, example specifications are given based on Demoney and verification is discussed. Finally, Section 14.6 summarises this chapter.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this chapter
Cite this chapter
Mostowski, W. (2007). The Demoney Case Study. In: Beckert, B., Hähnle, R., Schmitt, P.H. (eds) Verification of Object-Oriented Software. The KeY Approach. Lecture Notes in Computer Science(), vol 4334. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69061-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-69061-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68977-5
Online ISBN: 978-3-540-69061-0
eBook Packages: Computer ScienceComputer Science (R0)