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

Siddhartha Bhattacharyya
(Florida Institute of Technology)
Jennifer Davis
(Collins Aerospace)
Anubhav Gupta
(University of British Columbia)
Nandith Narayan
(Florida Institute of Technology)
Michael Matessa
(Collins Aerospace)

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.

In Marie Farrell and Matt Luckcuck: Proceedings Third Workshop on Formal Methods for Autonomous Systems (FMAS 2021), Virtual, 21st-22nd of October 2021, Electronic Proceedings in Theoretical Computer Science 348, pp. 150–166.
Published: 21st October 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.348.11 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org