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

SB_UTM_6

Specification Description

The longitude (fpLon) of any UAS's waypoint in its flight plan will be bounded between MaxLonLB and MinLonUB.

Signals Required

fpLon

Boolean Conversion of Signals to Atomic Inputs

fpLon_leq_MaxLonUB = 1;
for(i = 0; i < NumUAS; i++)
{
    for(j = 0; j < NumWP[i]; j++)
    {
        // if UAS i's fpLon is greater than the upper bounded
        // and the value is not "nan"
        if((fpLon[i] > MaxLonUB) && (fpLon[i] == fpLon[i])
        { 
            fpLon_leq_MaxLonUB = 0;
        }
    }
} 
fpLon_geq_MinLonLB = 1;
for(i = 0; i < NumUAS; i++)
{    
    for(j = 0; j < NumWP[i]; j++)
    {
        // if UAS i's fpLon is less than the lower bounded
        // and the value is not "nan"
        if((fpLon[i] < MinLonLB) && (fpLon[i] == fpLon[i])
        { 
            fpLon_geq_MinLonLB = 0;
        }
    }
}

MLTL Specification

Original: (fpLon_leq_MaxLonUB ∧ fpLon_geq_MinLonLB)

Fault Explanation

The longitude from a UAS's flight plan is not physically possible.

Additional Notes

Longitude can only ever by between -180 and 180 degrees. Anything outside these bounds is nonsensical and indicates a fault within the system.

Figures

Figure 1: All of the flight plan's longitude (fpLon) waypoints from each GCS the UTM reads from the waypoint flight plan datatable.
Figure 2: The output of R2U2's monitoring of specification SB_UTM_6, confirming that no longitude waypoint from a UAS's flight plan exceeds its sensor bounds.
Figure 3: Since Fig. 1 had no fpLon inputs that exceeded MaxLonUB or MinLonLB, we manually injected a fault into a single flight plan's waypoint (purple).
Figure 4: The output of R2U2's monitoring of specification SB_UTM_6, showing that R2U2 catches when the injected fault occurs.