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. Scientists at USRA's Research Institute for Advanced Computer Science 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.
USRA 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).