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_2

Specification Description

The waypoint longitude (wpLon) of any UAS's telemetry data will be bounded between MaxLonLB and MinLonUB.

Signals Required

wpLon

Boolean Conversion of Signals to Atomic Inputs

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

MLTL Specification

Original: (wpLon_leq_MaxLonUB ∧ wpLon_geq_MinLonLB)

Updated: ☐[0,3] (wpLon_leq_MaxLonUB ∧ wpLon_geq_MinLonLB)

Fault Explanation

A UAS's waypoint longitude 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 waypoint longitude (wpLon) inputs from each GCS the UTM reads from the telemetry datatable.
Figure 2: The output of R2U2's monitoring of specification SB_UTM_2, confirming that no UAS exceeds its waypoint longitude sensor bounds.
Figure 3: Since Fig. 1 had no wpLon inputs that exceeded MaxLonUB or MinLonLB, we manually injected a fault into a single UAS (purple).
Figure 4: The output of R2U2's monitoring of specification SB_UTM_2, showing that R2U2 catches when the injected fault occurs. However, notice that there is bouncing in the initial Boolean specificaiton, which can lead to undesireable false-positive alerts.
Figure 5: The output of R2U2's monitoring of the updated specification SB_UTM_1, showing that R2U2 catches when the injected fault occurs and the "☐[0,3]" temporal operator acts as a sliding filter, debouncing R2U2's output.