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_10

Specificaiton Description

The longitude reference waypoint (wpLon) that any UAS is flying towards will be bounded between LON_LB and LON_UB

Signals Required

wpLon

Boolean Conversion of Signals to Atomic Inputs 

wpLon_leq_LonUB: wpLon ≤ LonUB
wpLon_geq_LonLB: wpLon ≥ LonLB

MLTL Specificaiton

wpLon_leq_LongUB ∧ wpLon_geq_LonLB

Fault Explanation

Any reference waypoint should be within the UTM's airspace

Additional Notes

Figures

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