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_2

Specification Description

The Start time of any flight plan must be less than the flight plan's End time

Signals Required

Start, End

Boolean Conversion of Signals to Atomic Inputs

Start_leq_End = 1;
for(i = 0; i < NumUAS; i++)
{
    // if UAS i's Start is less than its End
    // and both values are not "nan"
    if((Start[i] > End[i]) && (Start[i] == Start[i]) && (End[i] == End[i]))
    { 
        Start_leq_End = 0;
    }
}

MLTL Specification

Original: Start_leq_End

Fault Explanation

The user should not be able to say they landed before they took off

Additional Notes

Figures

Figure 1: The difference between a flight plan's start (Start) and end (End) times (End - Start) from each GCS the UTM reads from the operational flight plan datatable.
Figure 2: The output of R2U2's monitoring of specification OR_UTM_2, confirming that no flight plan's start time (Start) preceeds its end time (End).
Since Fig. 1 had no flight plans where Start preceeds End, we manually shift the End of a single flight plan (purple) so that it comes before Start.
Figure 4: The output of R2U2's monitoring of specification OR_UTM_2, showing that R2U2 catches when the injected fault occurs.