Flight critical software is safety critical and is expensive to maintain. NASA exploration missions to the moon, Mars and beyond will increasingly rely on highly capable software to achieve greater levels of autonomy and robustness. Managing the risk in an affordable manner is one of the greatest challenges for the space agency.

Our teams are developing and testing technologies that automate mathematical approaches for the analysis and generation of mission-critical software. These projects target sustained engineering, achieving affordable reliability over successive spirals of missions software development, and maintenance and upgrades for mission-critical software.

C Global Surveyor
Finding runtime errors with high precision in large software systems without executing the program 

JavaPathfinder
Uncovering subtle errors in complex next-generation avionics and space flight software

Synthesis
Generation dependable programs in complex domains that carry their own certification

System Level Verification
Scalable verification techniques for autonomous systems through divide and conquer 

Runtime Verification
Detecting subtle temporal errors from execution traces, including 'footprints' of bugs

Adaptive Control V&V
Validation and monitoring of convergence and stability of adaptive control based on neural nets

 

Downloadable Data Sheets on the Following Technologies

Verification and Validation for ISHM
Automated Software Synthesis
Verification & Validation of Adaptive Control Systems
Reliable and Secure Space Communication Protocols