Automated Software Verification

Software V&V Toolkit – SGT engineers have been conducting research for NASA on advanced software V&V technologies for many years, developing tools based on this research, and maturing and applying these as well as off-the-shelf software verification technologies to countless NASA vehicles and missions as part of NASA’s Software V&V Toolkit. The prime benefit has been reduction of the risk of mission failure by identification of software issues through use of advanced V&V technologies. SGT has supported development of an open source community of V&V researchers and collaborators focused on the NASA R&D team’s technologies, thus leveraging NASA’s investments. Lessons learned and process improvements are directly integrated back into research activities to improve tools and techniques.

Non-Advocate Assessment – At NASA Ames Research Center, under the SGT ISRDS prime contract, SGT is performing a Non-Advocate Assessment (NAA) of various aspects of NASA/NOAA Geostationary Operational Environmental Satellite-R (GOES-R) Series Program’s Ground Segment (GS) development. The GOES-R GS is an integrated, distributed IT system that will conduct satellite operations and sensor product generation and distribution. SGT’s assessments ensure that the GS is performing to defined design, cost, schedule and performance specifications/capabilities. Activities include requirements, preliminary and all future reviews of the relevant mission-critical software.

IV&V – At the Volpe National Transportation System Center, under the SGT V-TRIPS prime contract, we support IV&V Discovery and Fact-finding Projects in support of the FAA’s Air Traffic Organization, Air Traffic Systems. SGT developed a Phase-based IV&V approach beginning with historical and current state investigatory meetings. Our work includes evaluating test reports, Version Description Documents and software problem reports to assess issue adjudication and associated risk.

SENSOR – For the Air Force Space Command (AFSPC), under subcontract to ITT, SGT supports IV&V activities including assessments, process and procedure audits, project and performance management, and systems analysis and design on a range of sensor projects involving IT systems at Eglin Air Force Base. SGT provides IV&V support during developer component/subsystem testing and validation and process support through government briefings and decision boards.

Java Pathfinder (JPF) – JPF is an advanced software model checking system that has been under development by SGT personnel at NASA Ames Research Center for more than a decade. JPFwas open sourced in 2005, has a large international user community, and has spawned academic and industrial collaborations around the globe. In 2009, JPF won the “Outstanding Technology Development” award of the Federal Laboratory Consortium (FLC). JPF is implemented as a virtual machine for Java™ bytecode programs. The defining qualityof the system is its extensibility:

  • Plugins allow easy creation of new checks for specific defects
  • Libraries can be abstracted to increase verif cation efficiency
  • Execution semantics of bytecode instructions can be modified to support capabilities such as symbolic values
  • Choice types and values such as scheduling sequences or input values can be configured

Now in its 6th release cycle, JPF has been instrumental in finding hard-to-test software defects both inside and outside of NASA, and is poised to become a mainstream asset to ensure proper functioning of your safety and security critical applications.