Automated Software Verification & Validation: An Emerging Approach for Ground Operations

Software is an increasingly critical component in aerospace systems, and automated software testing technologies that use formal methods are emerging as a new type of ground data system for verifying and validating software changes. With each change made to software for use in operational settings, there is the opportunity for new bugs to be introduced that can cause potentially catastrophic results. This research has evolved two formal method approaches for automated software verification and validation model checking and static analysis, with extensions of the approaches for multiple languages including Java, C and C++. The research is removing the barriers to routine use of formal methods to gain high assurance for human-rated space missions. These methods have been used on control software for a variety of mission critical systems including guidance, navigation and control (GN&C) subsystems, and for various projects such as the NASA Crew Exploration Vehicle (CEV).