Run-Time Assurance for Learning-Based Aircraft Taxiing

Aircraft systems that include learning-enabled components (LECs) and their software implementations are not amenable to verification and certification using current methods. We have produced a demonstration of a run-time assurance architecture based on a neural network aircraft taxiing application that shows how several advanced technologies could be used to ensure safe operation. In this paper we report on the use of a run-time assurance architecture based on the ASTM F3269-17 standard for bounded behavior of complex systems, also known as a simplex architecture. Our implementation of the standard includes:

• System architecture modeled using the Architecture Analysis and Design Language (AADL)
• Formal verification of system behaviors using the Assume Guarantee Reasoning Environment (AGREE)
• Architecture-based assurance case for showing correct implementation using Resolute
• Diverse run-time monitors for system safety, integrity, and availability
• Synthesis from formal specifications with proof of correctness for critical high-assurance components