Assuring Increasingly Autonomous Systems in Human-Machine Teams: An Urban Air Mobility Case Study
Open Access
- 21 October 2021
- journal article
- Published by Open Publishing Association in Electronic Proceedings in Theoretical Computer Science
- Vol. 348, 150-166
- https://doi.org/10.4204/eptcs.348.11
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.This publication has 16 references indexed in Scilit:
- Crew Resource Management Doctrine Applicability to Human-Machine Interaction in Commercial AircraftPublished by Springer Science and Business Media LLC ,2017
- Do Age and Experience Level Affect Views of Pilots’ Towards Cockpit AutomationAdvances in Intelligent Systems and Computing, 2017
- Using a Crew Resource Management Framework to Develop Human-Autonomy Teaming MeasuresAdvances in Intelligent Systems and Computing, 2017
- Capturing Safety Requirements to Enable Effective Task Allocation between Humans and Automaton in Increasingly Autonomous SystemsPublished by American Institute of Aeronautics and Astronautics (AIAA) ,2016
- The nuXmv Symbolic Model CheckerLecture Notes in Computer Science, 2014
- Your "What" Is My "How": Iteration and Hierarchy in System DesignIEEE Software, 2012
- Guidelines for conducting and reporting case study research in software engineeringEmpirical Software Engineering, 2008
- Z3: An Efficient SMT SolverLecture Notes in Computer Science, 2008
- Minimal Assignments for Bounded Model CheckingLecture Notes in Computer Science, 2004
- ACT-R: A Theory of Higher Level Cognition and Its Relation to Visual AttentionHuman–Computer Interaction, 1997