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

CS_GCS_3

Specification Description

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

Signals Required

LatWP, LonWP, fpLat, fpLon

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