Verification and Validation for Java Classes using Design by Contract. The Modular External Approach

Authors: Dario Ramirez de Leon, Oscar Chavez Bosquez, Julian J. Francisco Leon

Abstract:

Since the conception of JML, many tools, applications and implementations have been done. In this context, the users or developers who want to use JML seem surounded by many of these tools, applications and so on. Looking for a common infrastructure and an independent language to provide a bridge between these tools and JML, we developed an approach to embedded contracts in XML for Java: XJML. This approach offer us the ability to separate preconditions, posconditions and class invariants using JML and XML, so we made a front-end which can process Runtime Assertion Checking, Extended Static Checking and Full Static Program Verification. Besides, the capabilities for this front-end can be extended and easily implemented thanks to XML. We believe that XJML is an easy way to start the building of a Graphic User Interface delivering in this way a friendly and IDE independency to developers community wich want to work with JML.

Keywords: Model checking, verification and validation, JML, XML, java, runtime assertion checking, extended static checking, full static program verification.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1332750

References:

[1] Gary T. Leavens-s Home Page, http://www.cs.ucf.edu/~leavens/ homepage.html
[2] P. Chalin, P. R. James, and G. Karabotsos: JML4: Towards an Industrial Grade IVE for Java and Next Generation Research Platform for JML. In: Proceedings of the International Conference on Verified Software: Theories, Tools, Experiments (VSTTE). Toronto, Canada, Oct. 6-9 (2008)
[3] P. Chalin, P. R. James, and G. Karabotsos: An Integrated Verification Environment for JML: Architecture and Early Results. In: Proceedings of the Sixth International Workshop on Specification and Verification of Component-Based Systems (SAVCBS), Cavtat, Croatia, Sept. 3-4 (2007)
[4] Krakatoa and Jessie: verification tools for Java and C programs, http: //krakatoa.lri.fr/
[5] OpenJML jmlspecs, http://sourceforge.net/apps/trac/jmlspecs/wiki/ OpenJml
[6] JML4c, http://www.cs.utep.edu/cheon/download/jml4c/index.php
[7] JMLRAC, http://www.eecs.ucf.edu/~leavens/JML2/docs/man/jmlrac. html
[8] Yoonsik Cheon, Gary T. Leavens: A runtime assertion checker for the Java Modeling Language (JML). In: Proceedings of the International Conference On Software Engineering Research and Practice (SERP 02), Las Vegas, Nevada, USA, June 24-27 (2002)
[9] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata: Extended Static Checking for Java. In Programming Language Design and Implementation (PLDI) 2002 forum. http://research.microsoft.com/en-us/um/people/leino/papers/krml103.pdf
[10] Why platform, http://why.lri.fr/
[11] C. Oriat. Jartege: A Tool for Random Generation of Unit Tests for Java Classes In Quality of Sofware Architectures and Software Quality, 2nd International Workshop of Software Quality SOQUA05, LNCS 3712, pages 242-256, Erfurt, Germany, Sept 2005.
[12] JML Tools Review & Evaluation, http://www.cs.colorado.edu/~bec/ courses/csci5535-s10/slides/grosshans-lewis-prazen.2up.pdf
[13] JMLEclipse - jmlspecs, http://sourceforge.net/apps/trac/jmlspecs/wiki/ JmlEclipse
[14] The OpenJML User Guide, page 13, http://jmlspecs.sourceforge.net/ OpenJMLUserGuide.pdf
[15] Extensible Markup Language (XML), http://www.w3.org/XML/
[16] del Mar Gallardo, M., Mart'ınez, J., Merino, P., Nu˜nez, P. and Pimentel, E.: PiXL: Applying XML Standards to Support the Integration of Analysis Tools for Protocols. In Science of Computer Programming Journal, Volume 65, Issue 1, 57-69 (March 2007). http://www.lcc.uma.es/~pedro/publications/pixl gallardo.pdf