Formal Verification of a Machine Learning Tool for Runway Configuration Assistance

This study explores the use of formal verification techniques to evaluate the efficacy of suggestions made by the Runway Configuration Assistance (RCA) tool, a machine learning-based decision support system that our group developed independently Memarzadeh et al. (2023). By using model-checking approaches, in particular Computation Tree Logic (CTL), this study verifies the compliance of the RCA tool with predefined safety regulations under different conditions of surface winds. By simulating a range of scenarios at three major US airports, Charlotte Douglas International Airport (CLT), Denver International Airport (DEN), and Dallas-Fort Worth International Airport (DFW), we thoroughly test the predictions of the tool to ensure that they meet strict safety margins with respect to crosswind and tailwind. The application of formal verification methods provides a strict analysis of the RCA tool, enhancing its validity and utility for possible implementation in an operational environment. Initially, a Monte Carlo simulation is carried out to analyze all possible wind conditions both velocity-wise and direction-wise. This part is intended to rigorously test the model against extreme, worst-case conditions to evaluate its performance. Second, we improve our methodology by performing simulations driven by realistic scenarios informed by actual historical data. This approach allows for a more accurate reflection of typical wind conditions (seen in the test airport) and provides a robust assessment of the model’s effectiveness in maintaining safety standards under realistic environmental conditions. The model-checking reveals that overall 70% and 94% of the predictions satisfy the safety criteria in worst-case and realistic wind scenarios, respectively.