NASA Innovation Award
ITSR's Java PathFinder (JPF) model checker wins NASA's “Engineering Innovation” Turning Goals Into Reality (TGIR) award for 2003.
Research Task: High-Assurance Software Design (ITSR/ASET)
Principal Investigator: Willem Visser, Ph.D., NASA Ames Research Center
The Challenge
Software is an enabling technology for NASA, and constitutes a substantial portion of an aircraft or spacecraft's total cost. Most of the software cost goes to testing. For example, assuring that software will meet FAA certification requirements can account for more than 50% of the total software development cost. For this reason, many advances in software development—object orientation, concurrency, and dynamic creation and scheduling—are not being used in flight software today because conventional testing techniques cannot certify them. Yet these new systems could dramatically reduce the cost of software. For example, Integrated Modular Avionics (IMA) will reduce the cost of flight computers, but it requires the use of dynamic scheduling and concurrency. Similarly, autonomous planning and scheduling will enable deep-space missions to proceed without constant monitoring from Earth, but these systems must also be certified for safety and reliability.
Award-Winning Java PathFinder (JPF)
To meet this challenge, the ITSR Project's High-Assurance Software Design research team, led by Willem Visser, has developed a revolutionary tool—Java PathFinder (JPF). The JPF model checker recently received NASA's “Engineering Innovation” Turning Goals Into Reality (TGIR) award for 2003. JPF is an advanced testing tool for Java developed by ITSR's Automated Software Engineering Technologies (ASET) subproject. The development team consists of researchers from RIACS, Kestrel Technologies and NASA Ames Research Center. Their motivation for developing the tool was the fact that current techniques fall short of what is needed to meet FAA guidelines for certifying flight software. JPF shows that a model checker operating at the source-code level can uncover subtle behavioral errors in programs. For example, JPF found a subtle time-partitioning error in a new IMA-based DEOS real-time operating system, developed for use in small business aircraft. The error had escaped detection during conventional testing.
JPF can automatically detect errors in Java programs. It achieves better behavioral coverage than traditional testing tools for programs containing modern programming features. It is automatic, and, unlike traditional testing tools, when it finds an error it allows the developer to replay the error-prone scenario. JPF has been applied to software both inside and outside of NASA.
Technical Accomplishments
JPF is based on a technique, called model checking, that exhaustively analyzes a graph of a system's reachable states to check whether certain behavioral properties hold. Model checking has received a lot of attention in the hardware community. Companies such as Intel, IBM and Motorola have realized the potential of such tools, but hardware systems are mostly static; the JPF team was the first to use model checking to analyze object-oriented and dynamic software systems. To accomplish this, they had to overcome the technical difficulty of efficiently capturing the state of a program, especially of a very large program that can grow and shrink during its execution.
To do this, the team developed a novel compression algorithm that exploits the fact that most parts of the system state are not affected when executing a statement in the program. A common problem of model checking, and particularly acute in software model checking, is that there are a large number of possible system states (called the “state-explosion”). The JPF team observed that a large body of work already existed on how to use static analysis to enable better compilation of programs. The team used these techniques to reduce the size of the programs under analysis. To reduce the effect of the state–space explosion, the team combined ideas from abstract interpretation, alias analysis and slicing. To further improve the efficiency of error discovery, they used ideas from the artificial intelligence field; they used intelligent search algorithms to look only at those portions of the program most likely to contain errors.
In addition to the DEOS operating system JPF has been used to analyze, and find errors in, a number of flight software systems under development at NASA. JPF is currently being considered for use in analyzing Space Shuttle (ground) software.
More About the Award-Winning JPF Team
The ITSR–funded project is a joint venture between the Automated Software Engineering group at NASA Ames and four universities: Kansas State University, Carnegie Mellon University (CMU), the Massachusetts Institute of Technology (MIT), and the State University of New York (SUNY) at Stony Brook. The JPF team members include Mike Lowry and John Penix of NASA Ames Research Center; Willem Visser, Dimitra Giannakopoulou, and SeungJoon Park of the Research Institute for Advanced Computer Science (RIACS), and their associate summer student researchers—Flavio Lerda (CMU), Alex Groce (CMU), and Sarfraz Khurshid (MIT); Klaus Havelund, Corina Pasareanu, and Guillaume Brat of Kestrel Technologies; Matt Dwyer, John Hatcliff, Roby Joehanes, and Oksana Tkachuk of Kansas State University; and Scott Stoller of SUNY Stony Brook.
JPF was first released to beta testers in June 2001 by the NASA Ames Commercial Technology Office. There are currently more than 100 installations of the tool worldwide. Honeywell has started its own group to analyze future versions of the DEOS operating system based on the work of the JPF team, and a team from NASA's Engineering for Complex Systems (ECS) Program has been formed at NASA Ames to promote use of the tool throughout NASA.
The JPF team has also organized a number of workshops on software model checking in the U.S. and abroad. The team believes that these workshops, combined with the project's success, have had a substantial impact on the large number of companies and universities now actively pursuing research on software model checking.
Read other Technology Spotlight stories...
Top
