Software Challenges in Aerospace at AIAA SciTech 2017 featured a panel on “Verification versus Certification for Software Intense Systems” on January 9, 2017. The panel consisted of Ella Atkins (University of Michigan), Natasha Neogi (NASA Headquarters), Andre Platzer (CMU), and Kristin Yvonne Rozier (ISU). The panel was chaired by Misty Davies (NASA Ames), and Christoph Torens (DLR).
The Laboratory for Temporal Logic is particularly concerned with both design time verification to enable certification and “Adding Runtime Verification without Losing Certification,” which was the topic of the presentation by Prof. Kristin Yvonne Rozier. Today, there is a big push to quickly deploy many new types of small and cheap systems, including UAS, small satellites, helper technologies like software to suggest conflict resolutions to air traffic controllers, and automated co-pilot procedures in aircraft cockpits. Also, rovers on Earth may be small and cheap, or even disposable such as if they are meant to be deployed to hazardous environments unsafe for humans. These (semi-) autonomous systems require verification but are often composed of COTS or similarly already-certified components, eliminating the opportunity to utilize design-time verification as an enabler to certification. Also, the nature of the missions of small and cheap systems like these may not be amenable to full formal verification due to limited time, limited cost, and their expendability. Therefore, it is important to ask how do we verify an certify small and cheap systems? How are verification and certification different for autonomous systems? And how can verification enable, or at least not hinder, certification? This talk proposed some ideas for addressing these questions via the R2U2 framework and pointed to important areas for future research.