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_GCS_3

Specification Description

The Start time of any flight plan should be greater than the Time_Filed of the flight plan

Signals Required

Start, Time_Filed

Boolean Conversion of Signals to Atomic Inputs

Start_geq_TimeFiled = True;
for(i = 0; i < NumWp; i++)
{
    if(Start < Time_Filed[i])
    {
        Start_geq_TimeFiled = False;
    }
}						

MLTL Specification

Start_geq_TimeFiled

Fault Explanation

You cannot file a flightplan that started in the past

Additional Notes

Figures