Fujitsu Develops Technology to Enhance Comprehensive Testing of Java Programs

Sunnyvale, U.S. and Kawasaki, Japan, January 12, 2010

Fujitsu Laboratories of America, Inc. and Fujitsu Laboratories Ltd. today announced Fujitsu's development of a technology for comprehensively testing Java-based programs, which requires no manual effort to generate input values covering a wide range of possible input data. The new technology builds on Symbolic Java PathFinder⁽¹⁾, a software verification system developed by NASA, and expands it by adding efficient handling of not only numerical data, but also text data as input values. Such input data are extensively used in web applications. NASA will partially internally employ this new technology from Fujitsu and open-source it.

Background

As part of NASA's aerospace technology development efforts, it conducts R&D on software used to control systems. At its Ames Research Center, NASA conducts research on software-verification technology for determining whether programs are written correctly. As part of this effort, NASA developed Java PathFinder, a verification tool for testing software coded in Java. Java PathFinder is used to test the control systems for a Mars probe, and was released as open source in 2005. Thanks to its built-in interface for extensions, Fujitsu Laboratories, among other corporations and academic institutions, has used Java PathFinder as a framework for Java verification tools.

Technological Challenges

Verification of whether a program operates according to specifications typically requires significant manual effort to generate massive amounts of data for testing. In addition, an enormous amount of time is spent to conduct the testing.

Java PathFinder features a function called "symbolic execution mode", a function that makes it possible to automatically execute operations that arise when a wide range of input data variations are used, without the need to provide explicit test data. In this mode, it is known as Symbolic Java PathFinder. The main goal of Symbolic Java Pathfinder is test input generation. Java PathFinder has gained acceptance since its introduction in 2001.It offers features that generate test data that can cover all operational conditions, and that can automatically verify whether particular application specifications are satisfied.

In the past, Java Pathfinder supported solely numerical data in its symbolic execution mode and was unable to handle text strings. In order to make Java Pathfinder applicable to business applications, which typically deal with processing a great deal of text data, it would need to support such data.

Fujitsu's New Technology

To address the aforementioned issue, Fujitsu Laboratories developed a technology for supporting text strings in Java PathFinder's symbolic execution mode, making it more broadly applicable for verification. Key features of the new technology are as follows:

1. Method for modeling text strings that are extensively used in business applications
Numeric input data - such as bank account numbers - are processed in applications as text strings, and verification needs to check whether an unexpected text code was entered, whether the length of the input string complies with designated specifications, etc. The newly developed technology includes a method for "modeling" text strings, automatically extracts their parameters and expresses them in a compact format, which allows for efficient and comprehensive symbolic execution.

2. Expandable common interface
Fujitsu Laboratories also developed a common interface to extend the symbolic execution function to support text data. This enables Java PathFinder developers to easily extend the modeling method in symbolic execution mode for text data.

Results

This technology made it possible to conduct very comprehensive testing of software for web applications and other enterprise systems, where there is a growing demand for improved quality throughout the market. In actual testing conducted by Fujitsu Laboratories, this was found to be effective on Java-based web applications with tens of thousands of lines of code, and greatly increased the comprehensiveness of testing compared to conventional manual methods.

Regarding the power of the modeling process, Dr. Edmund Clarke, co-recipient of the 2007 A.M. Turing Award⁽²⁾ sponsored by the Association for Computing Machinery (ACM), conveyed the following remarks:

"I'm delighted to see this development by Fujitsu based on the NASA open-sourced software to advance the field of software verification", says Edmund Clarke, co-recipient of the 2007 Turing award for his pioneering research in model checking. "Their innovative use of symbolic execution, software model checking and string analysis to analyze industrial scale web-based systems is a major advance in the field."

Open Source Release

The text-handling functional extension to NASA's Java PathFinder represents a significant functional enhancement, and releasing as open source the common interface portion will make it possible for developers and researchers to use Java PathFinder with symbolic execution for text input data. It is anticipated that this new technology from Fujitsu will also enable acceleration of technological developments in software verification.

Future Developments

Fujitsu will continue with verification of large-scale, complex Java applications, striving for full-use practical application of this new technology.