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_14

Specification Description

The altitude (Alt) of any UAS's telemetry data will be bounded between 0.0 and ALT_UB

Signals Required

Alt

Boolean Conversion of Signals to Atomic Inputs

Alt_leq_AltUB: Alt ≤ AltUB
Alt_geq_0: Alt ≥ 0.0

MLTL Specification

Alt_leq_AltUB ∧ Alt_geq_0

Fault Explanation

Any telemetry point should be within the UTM's airspace

Additional Notes

Figures