Human-Computer Interface Concepts for Verifiable Mission Specification, Planning, and Management
Clayton D. Rothwell, Alexa Eggert, Michael J. Patzek, George Bearden, Gloria L. Calhoun, Laura R. Humphrey · 2013
Operators of unmanned aerial vehicles (UAVs) may soon be controlling multiple sophisticated autonomous systems in complex, dynamic mission contexts. A vital element for successful collaboration between human and autonomous agents is communication, which could be improved through the use of formal methods such as model checking. In model checking, the desired behavior of an autonomous system is specified using temporal logic, and a tool called a model checker is used to verify that the desired behaviors can be carried out by the system. Formal methods themselves, however, are challenging to learn and use but could be adapted to improve usability. This paper introduces a tool for writing formal specifications in a natural language representation, automatically translating them to temporal logic, and interfacing with model checking software. This tool is implemented within a UAV ground control station testbed and can be used for mission planning and monitoring. The tool and overall system are described and qualitatively compared to other tools designed to increase the usability of formal methods via translation of temporal logic.