Is this project an undergraduate, graduate, or faculty project?
Undergraduate
group
What campus are you from?
Daytona Beach
Authors' Class Standing
Alexandra Davidoff, Senior Juan Couder, Graduate Student Omar Ochoa, Faculty
Lead Presenter's Name
Alexandra Davidoff
Faculty Mentor Name
Dr. Omar Ochoa
Abstract
The development of Urban Air Mobility (UAM) infrastructure has garnered significant attention in recent years. Specifically, researchers have explored using Machine Learning (ML) technology to improve the efficiency and scalability of the UAM ecosystem. However, incorporating ML into safety-critical applications requires increased Verification and Validation (V&V) efforts to ensure safety to human life, an endeavor that is heavily scrutinized but not yet solved in current research. This paper proposes utilizing formal methods to verify ML systems integrated within UAM as a mitigation to safety concerns. We present brief surveys on ML trends within UAM and formal methods trends within UAM. We then combine these disciplines to argue for the usage of formal methods for ML verification in UAM while discussing modern trends within formal verification of ML systems. By utilizing formal methods alongside traditional verification techniques to verify ML systems, the safety and reliability of UAM can be increased. Therefore, this paper calls for further research into formal verification of ML within UAM.
Did this research project receive funding support from the Office of Undergraduate Research.
Yes, Spark Grant
Supporting Formal Methods for Machine Learning Verification in Urban Air Mobility
The development of Urban Air Mobility (UAM) infrastructure has garnered significant attention in recent years. Specifically, researchers have explored using Machine Learning (ML) technology to improve the efficiency and scalability of the UAM ecosystem. However, incorporating ML into safety-critical applications requires increased Verification and Validation (V&V) efforts to ensure safety to human life, an endeavor that is heavily scrutinized but not yet solved in current research. This paper proposes utilizing formal methods to verify ML systems integrated within UAM as a mitigation to safety concerns. We present brief surveys on ML trends within UAM and formal methods trends within UAM. We then combine these disciplines to argue for the usage of formal methods for ML verification in UAM while discussing modern trends within formal verification of ML systems. By utilizing formal methods alongside traditional verification techniques to verify ML systems, the safety and reliability of UAM can be increased. Therefore, this paper calls for further research into formal verification of ML within UAM.