Assuring Increasingly Autonomous Systems in Human-Machine Teams: An Urban Air Mobility Case Study

TL;DR

This paper presents a comprehensive methodology for verifying safety requirements of autonomous systems in urban air mobility, combining formal modeling, verification, and case studies to ensure safe human-machine teaming.

Contribution

It introduces a novel verification framework integrating formal models, automated translation, and case studies for autonomous urban air mobility systems.

Findings

Formal verification of safety requirements achieved for IAS and human team

Identification of design and requirements errors in the verification process

Lessons learned for future autonomous system safety assurance

Abstract

As aircraft systems become increasingly autonomous, the human-machine role allocation changes and opportunities for new failure modes arise. This necessitates an approach to identify the safety requirements for the increasingly autonomous system (IAS) as well as a framework and techniques to verify and validate that an IAS meets its safety requirements. We use Crew Resource Management techniques to identify requirements and behaviors for safe human-machine teaming behaviors. We provide a methodology to verify that an IAS meets its requirements. We apply the methodology to a case study in Urban Air Mobility, which includes two contingency scenarios: unreliable sensor and aborted landing. For this case study, we implement an IAS agent in the Soar language that acts as a copilot for the selected contingency scenarios and performs takeoff and landing preparation, while the pilot maintains final decision authority. We develop a formal human-machine team architecture model in the Architectural Analysis and Design Language (AADL), with operator and IAS requirements formalized in the Assume Guarantee REasoning Environment (AGREE) Annex to AADL. We formally verify safety requirements for the human-machine team given the requirements on the IAS and operator. We develop an automated translator from Soar to the nuXmv model checking language and formally verify that the IAS agent satisfies its requirements using nuXmv. We share the design and requirements errors found in the process as well as our lessons learned.