Defense Date
2026
Document Type
Dissertation
Degree Name
Doctor of Philosophy
Department
Electrical & Computer Engineering
First Advisor
Dr. Carl Elks
Abstract
The advent of the Urban Air Mobility (UAM) concept will bring low-altitude aviation to civilians through passenger and cargo transport. However, the prospective vehicles in UAM studies are predominantly autonomous, raising questions about their efficacy and stability in densely populated urban areas. At the same time, extensive work has been performed to define a new branch of systems engineering that focuses on runtime behavior, synchronization, communication, and task allocation.This field is known as "mission engineering". Mission engineering has been deployed in military scenarios to model human-autonomy cooperation. By applying the concepts from this field to UAM, full systems-of-systems can be described in the context of flight tasks alongside their human operators. These concepts may help build a foundational understanding of the UAM operational space and its entities. To verify this in the live environment, runtime verification (RV) is a key technology, which is frequently applied to unmanned aerial vehicles (UAVs) and is synergistic with the complexity of UAM operations. However, adequate formalisms derived from a mission model must be created in order to provide properties for a RV framework to monitor. This dissertation implements an ontological monitoring concept based around the elements of UAM missions. Applied ontology has seen increasing use in the 21st century as a method of describing entities and their relations. The RV framework produced in this work is driven by an applied ontology; we call its runtime monitors "ontological monitors." The ontological monitors are explicitly designed to verify mission execution through a custom ontology known as the Mission Ontology.This ontology is formalized into a set of properties in first-order logic for the behavior and relations of the ontological classes.These formal properties are then translated into "quantified temporal logic'' (or QTL). This allows the use of the runtime monitoring framework DejaVu, which uses QTL as its property specification language. To demonstrate these monitors, we utilize the VIRGO testbed, which is custom-built for the purpose of characterizing and validating runtime monitor performance in a UAV flight environment. We present three case studies, which demonstrate the use of the ontology to specify simple flight, task assignment, and a more complex AI-assisted search-and-rescue mission.
Rights
© The Author
Is Part Of
VCU University Archives
Is Part Of
VCU Theses and Dissertations
Date of Submission
8-6-2026