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_9

Specification Description

The latitude reference waypoint (wpLat) that any UAS is flying towards will be bounded between LAT_LB and LAT_UB

Signals Required

wpLat

Boolean Conversion of Signals to Atomic Inputs 

wpLat_leq_LatUB: wpLat ≤ LatUB
wpLat_geq_LatLB: wpLat ≥ LatLB

MLTL Specificaiton

wpLat_leq_LatUB ∧ wpLat_geq_LatLB

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