Assuring Increasingly Autonomous Systems in Human-Machine Teams: An Urban Air Mobility Case Study
This work tackles safety assurance for autonomous systems in critical domains like aviation, but it is incremental as it builds on existing formal verification and human-machine teaming techniques.
The paper addresses the safety verification of increasingly autonomous systems (IAS) in human-machine teams, specifically for Urban Air Mobility, by developing a formal methodology to identify and verify safety requirements, and applies it to contingency scenarios like unreliable sensors and aborted landings, finding design and requirement errors in the process.
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.