Verification and Validation for Java Classes using Design by Contract. The Modular External Approach
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.
[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
[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
@article{"International Journal of Information, Control and Computer Sciences:55944", author = "Dario Ramirez de Leon and Oscar Chavez Bosquez and Julian J. Francisco Leon", title = "Verification and Validation for Java Classes using Design by Contract. The Modular External Approach", 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.", volume = "6", number = "4", pages = "455-8", }
