The main goal of this project is to promote behavioral interface
specifications as a practical programming tool. For this, the project
has two objectives:
Our approach is to extend the
Java Modeling Language (JML),
a behavioral interface specification language (BISL) for Java
(see Figure 1) and experiment various
specification techniques and notations.
As stated above, tool development is an integral
part of our project, and in particular we are interested in runtime
assertion checking and its applications, such as specification-based
Yoonsik Cheon and several
of his graduate students are leading this project. Specific research topics
include the following:
- to develop practical techniques and notations to formally
specify the behaviors of Java program modules such as classes and
- to develop a set of practical support tools that can be
integrated into Java programming environments.
- Complete automation of unit
Myoung Kim, a Ph.D. student, is investigating specification-based
unit testing for Java. She is interested in fully automating unit
tests---from test case selection to execution and to outcome
An approach is proposed to combine interface specifications,
genetic algorithms, and a testing framework. The key idea is
to use postconditions as test oracles,
to generate test cases automatically by applying genetic algorithms,
and to use JUnit as a test execution platform.
- Specifying and checking method
Ashaveena Perumendla, a M.S. student, is extending JML to allow
one to specify and check at runtime the allowed sequences
of method calls. A new specification clause, called a
call sequence clause, is
introduced to constrain the order of method calls in a
regular expression-like notation.
The call sequence specifications are translated into finite state
machines for runtime assertion checking.
- Canica: An IDE for JML. Angelica Perez, a M.S. student, is
developing an integrated development environment (IDE) for JML
to provide a user-friendly graphical interface to a set of
command-line based tools.
Publications for related articles and papers.
An early proof-of-concept prototype of UTJML is available from
Software Download Page.
For Local Developers
Last modified: $Id: index.html,v 1.5 2007/06/15 21:56:09 cheon Exp $