design element
RIACS banner
 
section image top Outreach       
section image bottom     design element

 


RIACS News

RIACS Staff Receive Federal Laboratory Consortium for Technology Transfer Far West Region Outstanding Technology Development Award Award (12/9/2009) - Java Pathfinder

HIGHLIGHT:

USRA RIACS scientists have a worldwide reputation in the advanced techniques for software verification and validation, including the use of formal methods with support for traditional and non-traditional software (e.g neural network flight control software).

Software is an increasingly critical component in aerospace systems, and automated software testing technologies that use formal methods are emerging as a new approach for verifying and validating software for high levels of reliability, safety and security. USRA scientists in collaboration with the NASA Ames Research Center co-invented the first model checker for software testing directly on code ? Java Pathfinder (JPF); and were recently awarded a Federal Laboratory Consortium Technology Transfer Far West Region Outstanding Technology Development Award for this work. JPF is a verification system for high reliability Java programs, which automatically explores all possible execution paths of a program, and so is guaranteed to find those paths that result in defects. The system achieved this with a number of highly innovative implementations of state storage, state matching, partial-order reduction, and many more aspects of model checking. The system was first introduced in 2002, and was subsequently released as open source by NASA. The same approach has since been applied to other software programming languages, and can be utilized to automatically verify important properties of software systems. Currently, USRA scientists are engaging university partners for broader participation of the university community in common open source software V&V approaches.

 

 

design element
design element
design element
design element