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_13

Specification Description

The longitude (Lon) of any UAS's telemetry data will be bounded between LON_LB and LON_UB

Signals Required

Lon

Boolean Conversion of Signals to Atomic Inputs 

Lon_leq_LonUB: Lon ≤ LonUB
Lon_geq_LonLB: Lon ≥ LonLB

MLTL Specification

Lon_leq_LonUB ∧ Lon_geq_LonLB

Fault Explanation

Any telemetry point 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