Integrating Runtime Verification into an
Automated UAS Traffic Management System

Matthew Cauwels, Abigail Hammer, Benjamin Hertz, Phillip H. Jones, Kristin Y. Rozier

This webpage contains supplementary specifications for "Integrating Runtime Verification into an
Automated UAS Traffic Management System" by M. Cauwels, A. Hammer, B. Hertz, P. H. Jones, and K. Y. Rozier

OR_UTM_4

Specification Description

All latitude (fpLat) waypoints of any UAS's flight plan will be bounded between LatLB and LatUB.

Signals Required

fpLat

Boolean Conversion of Signals to Atomic Inputs 

fpLat_leq_LatUB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's fpLat[j] is greater than the upper bounded
    // and the value is not "nan"
    for(j = 0; j < NumWps[i]; j++)
    {
        if((fpLat([i,j] > LatUB) && (fpLat[i,j] == fpLat[i,j])
        { 
            fpLat_leq_LatUB = 0;
        }
    }
}                       
fpLat_geq_LatLB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's fpLat[j] is less than the lower bounded
    // and the value is not "nan"
    for(j = 0; j < NumWps[i]; j++)
    {
        if((fpLat[i,j] < LatLB) && (fpLat[i,j] == fpLat[i,j])
        { 
            fpLat_geq_LatLB = 0;
        }
    }
}

MLTL Specification

Original: fpLat_leq_LatLB ∧ fpLat_geq_LatLB

Fault Explanation

Any waypoint from the flight plan should be within the UTM's airspace

Additional Notes

Figures

Figure 1: All of the flight plan's latitude waypoints (fpLat) from each GCS the UTM reads from the waypoint flight plan datatable.
Figure 2: The output of R2U2's monitoring of specification OR_UTM_4, confirming that no UAS exceeds its operating range.
Figure 3: Since Fig. 1 had no flight plans where fpLat exceeds LatLB or LatUB, we manually injected a fault into a single flight plan's waypoint (purple).
Figure 4: The output of R2U2's monitoring of specification OR_UTM_4, showing that R2U2 catches when the injected fault occurs.