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_10

Specification Description

The altitude reference waypoint (wpAlt) that any UASs is flying towards will be bounded between AltLB and AltUB

Signals Required

wpAlt

Boolean Conversion of Signals to Atomic Inputs 

wpAlt_leq_AltUB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's wpAlt is greater than the upper bounded
    // and the value is not "nan"
    if((wpAlt[i] > AltUB) && (wpAlt[i] == wpAlt[i])
    { 
        wpAlt_leq_AltUB = 0;
    }
}                       
wpAlt_geq_AltLB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's wpAlt is less than the lower bounded
    // and the value is not "nan"
    if((wpAlt[i] < AltLB) && (wpAlt[i] == wpAlt[i])
    { 
        wpAlt_geq_AltLB = 0;
    }
}

MLTL Specification

Original: wpAlt_leq_AltLB ∧ wpAlt_geq_AltLB

Updated: ☐[0,3] (wpAlt_leq_AltLB ∧ wpAlt_geq_AltLB)

Fault Explanation

Any telemetry point should be within the UTM's airspace

Additional Notes

Figures

Figure 1: All of the reference altitude waypoints (wpAlt) inputs from each GCS the UTM reads from the telemetry datatable.
Figure 2: The output of R2U2's monitoring of specification OR_UTM_10, confirming that no UAS exceeds its operating range.
Figure 3: Since Fig. 1 had no wpAlt inputs that exceeded AltUB or AltLB, we manually injected a fault into a single UAS (purple).
Figure 4: The output of R2U2's monitoring of specification OR_UTM_10, showing that R2U2 catches when the injected fault occurs. However, notice that there is bouncing in the initial Boolean Specification, which can lead to undesireable false-positive alerts.
Figure 5: The output of R2U2's monitoring of the updated specification OR_UTM_10, showing that R2U2 catches when the injected fault occurs and the "☐[0,3]" temporal operator acts as a sliding filter, debouncing R2U2's output.