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_8

Specification Description

The reference latitude (LatWP), longitude (LonWP), and altitude (AltWP) will be contained within the set of waypoints given in the flight plan

Signals Required

LatWP, LonWP, AltWP, fpLat, fpLon, fpAlt

Boolean Conversion of Signals to Atomic Inputs

wpLonLat_eq_fpLonLat = False;
for (i = 0; i < NumWp; i++)
{
    if ((wpLon == fpLon(i)) && (wpLat == fpLat(i)))
         wpLonLat_eq_fpLonLat == True;
}						

MLTL Specification

wpLonLat_eq_fpLon_Lat

Fault Explanation

Reference waypoints should be contained within the set of waypoints from that UAS's flight plan (this spec will tell us if anyone deviated from their flight plan)

Additional Notes

Figures