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_6

Specification Description

All altitude (fpAlt) waypoints of any UAS's telemetry data will be bounded between 0.0 and ALT_UB

Signals Required

fpAlt

Boolean Conversion of Signals to Atomic Inputs

fpAlt_leq_AltUB: fpAlt ≤ AltUB
fpAlt_geq_0: fpAlt ≥ 0.0

MLTL Specification

fpAlt_leq_AltUB ∧ fpAlt_geq_0

Fault Explanation

Any waypoint from the flight plan should be within the UTM's airspace

Additional Notes

Figures