Executing JML specifications of Java card applications

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Executing JML specifications of Java card applications: a case study

Full text

Pdf (267 KB)

Source

Symposium on Applied Computing archive
Proceedings of the 2009 ACM symposium on Applied Computing table of contents

Honolulu, Hawaii

SESSION: Software engineering track table of contents

Pages 404-408

Year of Publication: 2009

ISBN:978-1-60558-166-8

Authors

Néstor Cataño	University of Madeira, Funchal, Portugal
Tim Wahls	Dickinson College, Carlisle, PA

Sponsor

SIGAPP: ACM Special Interest Group on Applied Computing

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 10, Downloads (12 Months): 49, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1529282.1529373 What is a DOI?

ABSTRACT

Executability provides an important mechanism for validating formal specifications and allows such specifications to serve as prototypes and test oracles. In this case study, we used the jmle tool to execute the JML specification of an electronic purse application written in the Java Card dialect of Java. This effort resulted in numerous improvements to the specification and to the jmle tool itself, as well as insight into how executability can contribute to the use of formal methods in the software development process.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	S. Abdennadher, E. Krämer, M. Saft, and M. Schmauss. JACK: A Java constraint kit. In M. Hanus, editor, Electronic Notes in Theoretical Computer Science, volume 64. Elsevier, 2002.
	2	F. Bouquet, F. Dadeau, B. Legeard, and M. Utting. Symbolic animation of JML specifications. In Proceedings of the International Conference on Formal Methods 2005 (FM'05), volume 3582 of Lecture Notes in Computer Science, pages 75--90. Springer-Verlag, July 2005.
	3	E. Bretagne, A. E. Marouani, P. Girard, and J.-L. Lanet. PACAP purse and loyalty specification. Technical Report V. 0.4, Gemplus, 2000.
	4	C.-B. Breunesse , N. Cataño , M. Huisman , B. Jacobs, Formal methods for smart cards: an experience report, Science of Computer Programming, v.55 n.1-3, p.53-80, March 2005 [doi>10.1016/j.scico.2004.05.011]
	5	Lilian Burdy , Yoonsik Cheon , David R. Cok , Michael D. Ernst , Joseph R. Kiniry , Gary T. Leavens , K. Rustan M. Leino , Erik Poll, An overview of JML tools and applications, International Journal on Software Tools for Technology Transfer (STTT), v.7 n.3, p.212-232, June 2005 [doi>10.1007/s10009-004-0167-4]
	6	Néstor Cataño , Marieke Huisman, Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods - Getting IT Right, p.272-289, July 22-24, 2002
	7	Néstor Cataño , Marieke Huisman, CHASE: A Static Checker for JML's Assignable Clause, Proceedings of the 4th International Conference on Verification, Model Checking, and Abstract Interpretation, p.26-40, January 09-11, 2002
	8	Patrice Chalin , Perry R. James , George Karabotsos, An integrated verification environment for JML: architecture and early results, Proceedings of the 2007 conference on Specification and verification of component-based systems: 6th Joint Meeting of the European Conference on Software Engineering and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, p.47-53, September 03-04, 2007, Dubrovnik, Croatia [doi>10.1145/1292316.1292322]
	9	L. du Bousquet , Y. Ledru , O. Maury , C. Oriat , J.-L. Lanet, A Case Study in JML-Based Software Validation, Proceedings of the 19th IEEE international conference on Automated software engineering, p.294-297, September 20-24, 2004 [doi>10.1109/ASE.2004.1]
	10	The ESC/Java 2 Tool. http://secure.ucd.ie/products/opensource/ESCJava2/.
	11	Wolfgang Grieskamp, A Computation Model for Z Based on Concurrent Constraint Resolution, Proceedings of the First International Conference of B and Z Users on Formal Specification and Development in Z and B, p.414-432, August 29-September 02, 2000
	12	Ian Hayes , C. B. Jones, Specifications are not (necessarily) executable, Software Engineering Journal, v.4 n.6, p.330-338, Nov. 1989
	13	The JACK Tool. http://www-sop.inria.fr/eve-rest/soft/Jack/jack.html.
	14	Daniel Jackson, Software Abstractions: Logic, Language, and Analysis, The MIT Press, 2006
	15	Java Card Technology. http://java.sun.com/products/javacard/.
	16	The Krakatoa Tool. http://krakatoa.lri.fr/.
	17	B. Krause and T. Wahls. jmle: A tool for executing JML specifications via constraint programming. In L. Brim, editor, Formal Methods for Industrial Critical Systems (FMICS '06), volume 4346 of Lecture Notes in Computer Science, pages 293--296. Springer-Verlag, August 2006.
	18	G. T. Leavens. The Java Modeling Language (JML) home page. http://www.jmlspecs.org.
	19	J. Link. Unit Testing in Java. Morgan Kaufmann, 2003.
	20	Microsoft Research. Executable specifications: Creating testable, enforceable designs, February 2001. http://research.microsoft.com/foundations/-ESpecTesting.doc.
	21	C. Oriat. Jartege, A Tool for Random Generation of Unit Tests for Java Classes. Technical Report RR1069, 2004.
	22	J. Robinson , Andrei Voronkov, Handbook of Automated Reasoning: Volume 1, MIT Press, Cambridge, MA, 2001
	23	Joachim van den Berg , Bart Jacobs, The LOOP Compiler for Java and JML, Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, p.299-312, April 02-06, 2001