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_4

Specification Description

All latitude (fpLat) waypoints of any UAS's flight plan will be bounded between LatLB and LatUB

Signals Required

fpLat

Boolean Conversion of Signals to Atomic Inputs 

fpLat_leq_LatUB: fpLat ≤ LatUB
fpLat_geq_LatLB: fpLat ≥ LatLB

MLTL Specification

fpLat_leq_LatUB ∧ pfLat_geq_LatLB

Fault Explanation

Any waypoint from the flight plan 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