Run-Time Assurance for Learning-Based Aircraft Taxiing

D. Cofer, I. Amundson, R. Sattigeri, A. Passi, C. Boggs, E. Smith, L. Gilham, T. Byun, S. Rayadurgam

Digital Avionics Systems Conference, October 2020

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