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_7

Specification Description

The Phase of any flight plan must be either START, STOP, HOME, or CRUISE

Signals Required

Phase

Boolean Conversion of Signals to Atomic Inputs

Phase_eq_Valid = False;
for(i = 0; i < NumWp; i++)
{
    if((Phase[i] == "START") ||
        (Phase[i] == "STOP") || 
        (Phase[i] == "HOME") || 
        (Phase[i] == "CRUISE"))
    {
        Phase_eq_Valid = True;
    }
}						

MLTL Specification

Phase_eq_Valid

Fault Explanation

The Phase (type of waypoint) is not valid. Only START, STOP, HOME, and CRUISE waypoints are valid waypoints in our current implementation of the UTM

Additional Notes

Figures