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_15

Specification Description

The velocity (Vel) of any UAS's telemetry data will be bounded between 0.0 and VEL_UB

Signals Required

Vel

Boolean Conversion of Signals to Atomic Inputs

Vel_leq_VelUB: Vel ≤ VelUB
Vel_geq_0: Vel ≥ 0.0

MLTL Specification

Vel_leq_VelUB ∧ Vel_geq_0

Fault Explanation

The speed of the UAS should be bounded

Additional Notes

Figures