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_21

Specification Description

The longitude (conLon) of any conflict will be bounded between LonLB and LonUB

Signals Required

conLon

Boolean Conversion of Signals to Atomic Inputs

conLon_leq_LonUB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's conLon is greater than the upper bounded
    // and the value is not "nan"
    if((conLon[i] > LonUB) && (conLon[i] == conLon[i])
    { 
        conLon_leq_LonUB = 0;
    }
}                       
conLon_geq_LonLB = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's conLon is less than the lower bounded
    // and the value is not "nan"
    if((conLon[i] < LonLB) && (conLon[i] == conLon[i])
    { 
        conLon_geq_LonLB = 0;
    }
}  

MLTL Specification

Original: conLon_leq_LonUB ∧ conLon_geq_LonLB

Updated: ☐[0,3] (conLon_leq_LonUB ∧ conLon_geq_LonLB)

Fault Explanation

Any conflict should be within the UTM's airspace

Additional Notes

Figures

Figure 1: All of the longitude (conLon) inputs from each GCS the UTM reads from the conflict datatable.
Figure 2: The output of R2U2's monitoring of specification OR_UTM_21, confirming that no conflict exceeds its operating range.
Since Fig. 1 had no conLon inputs that exceeded LonUB or LonLB, we manually injected a fault into a single conflict (orange).
Figure 4: The output of R2U2's monitoring of specification OR_UTM_21, 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 OR_UTM_21, showing that R2U2 catches when the injected fault occurs and the "☐[0,3]" temporal operator acts as a sliding filter, debouncing R2U2's output.