Abstract
In the context of the KeY program verifier and the associated Dynamic Logic for Java we discuss the first instance of applying a generalised approach to the treatment of memory heaps in verification. Namely, we allow verified programs to simultaneously modify several different, but possibly location sharing, heaps. In this paper we detail this approach using the Java Card atomic transactions mechanism, the modelling of which requires two heaps to be considered simultaneously – the basic and the transaction backup heap. Other scenarios where multiple heaps emerge are verification of real-time Java programs, verification of distributed systems, modelling of multi-core systems, or modelling of permissions in concurrent reasoning that we currently investigate for KeY. On the implementation side, we modified the KeY verifier to provide a general framework for dealing with multiple heaps, and we used that framework to implement the formalisation of Java Card atomic transactions. Commonly, a formal specification language, such as JML, hides the notion of the heap from the user. In our approach the heap becomes a first class parameter (yet transparent in the default verification scenarios) also on the level of specifications.
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
Amighi, A., Blom, S.C., Huisman, M., Zaharieva-Stojanovski, M.: The VerCors project: Setting up basecamp. In: 6th Workshop Programming Languages Meets Program Verification, pp. 71–82. ACM (2012)
B. Beckert, R. Hähnle, and P. H. Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Beckert, B., Mostowski, W.: A program logic for handling Java Card 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.R.M., Poll, E.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) 8th Int’l Workshop on Formal Methods for Industrial Critical Systems. ENTCS, vol. 80, pp. 73–89. Elsevier (2003)
Burdy, L., Requet, A., Lanet, J.-L.: Java applet correctness: A developer-oriented approach. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 422–439. Springer, Heidelberg (2003)
Chen, Z.: Java Card Technology for Smart Cards: Architecture and Programmer’s Guide. Addison-Wesley (June 2000)
Distefano, D., Parkinson, M.J.: jStar: towards practical verification for Java. SIGPLAN Notes 43, 213–226 (2008)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
Hubbers, E., Poll, E.: Reasoning about card tears and transactions in Java Card. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 114–128. Springer, Heidelberg (2004)
Jacobs, B., Smans, J., Philippaerts, P., Piessens, F.: The VeriFast program verifier – a tutorial for Java Card developers. Technical report, Department of Computer Science, Katholieke Universiteit Leuven, Belgium (September 2011)
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: A powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011)
Kassios, I.T.: Dynamic frames: Support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006)
Kwon, J., Wellings, A.J.: Memory management based on method invocation in RTSJ. In: Meersman, R., Tari, Z., Corsaro, A. (eds.) OTM-WS 2004. LNCS, vol. 3292, pp. 333–345. Springer, Heidelberg (2004)
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)
Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with Chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) Foundations of Security Analysis and Design, pp. 195–222. Springer (2009)
Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for certification of Java/Java Card programs annotated in JML. Journal of Logic and Algebraic Programming 58(1-2), 89–106 (2004)
Marché, C., Rousset, N.: Verification of Java Card applets behavior with respect to transactions and card tears. In: Hung, D.V., Pandya, P. (eds.) 4th IEEE Conference on Software Engineering and Formal Methods. IEEE Press (2006)
Mostowski, W.: Formal reasoning about non-atomic Java Card methods in dynamic logic. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 444–459. Springer, Heidelberg (2006)
Mostowski, W.: Fully verified Java Card API reference implementation. In: Beckert, B. (ed.) 4th Int’l Verification Workshop. CEUR WS, vol. 259 (2007)
Mostowski, W., Poll, E.: Malicious code on java card smartcards: Attacks and countermeasures. In: Grimaud, G., Standaert, F.-X. (eds.) CARDIS 2008. LNCS, vol. 5189, pp. 1–16. Springer, Heidelberg (2008)
Pallec, P.L., Saif, A., Briot, O., Bensimon, M., Devisme, J., Eznack, M.: NFC cardlet development guidelines v2.2. Technical report, Association Française du Sans Contact Mobile (2012)
Parkinson, M.J., Summers, A.J.: The relationship between separation logic and implicit dynamic frames. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 439–458. Springer, Heidelberg (2011)
Schmitt, P.H., Ulbrich, M., Weiß, B.: Dynamic frames in Java dynamic logic. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138–152. Springer, Heidelberg (2011)
Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 491–505. Springer, Heidelberg (2004)
Sun Microsystems, Inc., Java Card 2.2.2 Runtime Environment Specification (March 2006), http://www.oracle.com
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mostowski, W. (2013). A Case Study in Formal Verification Using Multiple Explicit Heaps. In: Beyer, D., Boreale, M. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2013 2013. Lecture Notes in Computer Science, vol 7892. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38592-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-38592-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38591-9
Online ISBN: 978-3-642-38592-6
eBook Packages: Computer ScienceComputer Science (R0)