Skip to content

Static Verification for J2EE-Based Software

J2EE is a set of Java-based technologies used to build applications accessible over the network. Flexibility and the ability to configure, based mainly on XML files, leads to the fact that more and more errors are beyond the control of the compiler.

Older systems described the interaction between parts of the system directly in the code and as such could you checked (at least partially) in the build phase by compiler. The trend to move this kind of information outside of Java code causes, unfortunately, many configuration errors will not be caught by compiler. Those errors will be visible later, at run time.

The complexity of the J2EE architecture makes the cycle (recompilation, installation, testing in a browser) long. This significantly makes the development method "change and run" harder. What can we do to speed up the process of developing J2EE applications?

(This is a translation of an article I wrote two years ago on static verification).

Static Verification

Static verification of software means "correctness proof" for average developer. The aim is to catch errors hidden in the system without actually running it. It should (theoretically) find all implementation bugs before testing phase. However, this idea contains some serious problems:

  • In practice, writing a formal specification of functionality is hard (mathematical background required)
  • Tools for verification are difficult to use and require a lot of practice for productive use
  • It's not possible to automatically checked against a formal specification, human intervention is required

As you can see the complete static verification is not feasible in typical systems. But can we take some benefits from the static verification ideas?

Resources in J2EE

Let's define "resource" term for the purpose of this article. It's an element of a J2EE application that can be analysed independently, and which relates to other resources after installation in the application server. An example of this resource is Java code, analysis is performed by the compiler during compilation. Example of such "resources":

  • Java code (no access regular expressions, the mechanism of reflection)
  • Struts configuration (no access: the SAX parser)
  • JSP files (no access: the SGML parser)
  • Setting up Tiles (no access: the SAX parser)
  • Translation in ApplicationResources_
  • *. properties (the standard Java library)
  • ...

Example: Struts static verification

What benefits can be achieved by statically and automatically analysis of above resource? Here are some common errors in J2EE/Struts applications, typically discovered after deployment:

  • Exception caused by using a page tag html: text property to the value of an attribute that does not exist as an attribute in the form-bean
  • Typo in the action attribute in the tag html: form, which causes confusion in the absence of a URL
  • No translation of static text appearing on the tag bean: message
  • Improper use of the name attribute in one of the tag causes an runtime exception

Finding such errors, especially when the project is subject to constant scope changes is inefficient and tiring. Wouldn't it be easier to get a complete list of these errors within a few seconds before deployment (instead of wasting time testers such obvious defects)?

I believe that the tester's job is to check compliance with specification, simple errors and typos should no longer appear in testing phase. How can we statically "catch" class of errors described above?

  • JUnit test that will match form-bean definitions (POJO classes) with html: text tags and check if properties called from JSP are present in Java class
  • Actions called from JSP can be compared to definitions in XML file
  • For each instance of the bean: message we can check whether there is an entry in the messages file
  • Every "name" used in JSP can be checked against bean list from Struts config file

Implementations

I was able to apply similar techniques for the following software configurations:

  • JSF: Java and JSP parsing based on regular expressions, the parser and verifier written in AWK
  • Struts: SGML parser for the JSP plus Java reflection API
  • Hibernate: static analysis of query parameters in the HQL vs bean class that hold query parameters

Also few implementations from outside Java world:

  • Zope ZPT templates: XML parser plus Python reflection API
  • Custom regexp-based rules checked against Python code

Summary

Static bug hunting means: early (before runtime) and with high coverage (not available by manual testing). It saves a lot of effort to track simple bugs and leave time for testers to do real work (check against specification).