AAHAA: Architecture and Analysis for High-Assurance Autonomy

Advanced capabilities planned for the next generation of autonomous unmanned vehicles will be based on non-traditional software components containing complex machine learning algorithms. These systems will incorporate adaptive and intelligent control algorithms that provide enhanced safety, autonomy, and high-level decision-making functions currently performed by human operators, as well as robustness in the presence of failures, adverse conditions, and unexpected situations.

Focusing on the aviation context, there are serious barriers to the deployment of autonomous aircraft, both in the military and in the National Airspace System (NAS). Current civil aviation certification processes are based on the idea that the correct behavior of a system or a component must be completely specified and verified prior to operation. Military aircraft acquisition processes make reference to civil certification processes and limitations. These barriers will delay or prevent the deployment of crucial safety functions and new capabilities that could be of great value in both military and civilian applications.

Collins Aerospace, Stanford University, Kestrel Institute, and University of Minnesota have teamed on DARPA's Assured Autonomy program to create new technologies for ensuring the safety of LECs in autonomous vehicle applications. These technologies include:

  • Architecture-driven assurance based on compositional reasoning about formally specified contracts for system components, including LECs
  • New formal verification methods that enable precise reasoning about LECs
  • Machine-checkable architecture-based assurance cases that encompass both design-time and run-time behaviors
  • Synthesis of run-time monitors for LECs
  • Safety-aware constraints on run-time adaptation of LECs
  • Architectural mitigation and enforcement techniques to guarantee safety in the presence of learning and adaptation
  • Assurance-optimized system test generation informed by analysis results

Models and code for the project are available on github.