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

SB_GCS_6

Specification Description

All fpLon will be bounded between -180 and 180 degrees

Signals Required

fpLon

Boolean Conversion of Signals to Atomic Inputs

fpLon_leq_MaxLonUB: fpLon ≤ MaxLonUB
fpLon_geq_MinLonLB: fpLon ≥ MinLonLB

MLTL Specification

¬☐[0,M] ¬(fpLon_leq_MaxLonUB ∧ fpLon_geq_MinLonLB)

Fault Explanation

Longitude is outside of predefined flightpath

Additional Notes

All Latitude and Longitude values should be actual Earth locations

Figures

Figure 1: Caption
Figure 2: Caption
Figure 3: Caption
Figure 4: Caption
Figure 5: Caption