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_16

Specification Description

The heading (Ang) of any UAS's telemetry data will be bounded between 0.0 and 360.0

Signals Required

Ang

Boolean Conversion of Signals to Atomic Inputs

Ang_leq_360: Ang ≤ 360.0
Ang_geq_0: Ang ≥ 0.0

MLTL Specification

Ang_leq_360 ∧ Ang_geq_0

Fault Explanation

The heading of the UAS should loop from 0 to 360 degrees

Additional Notes

Figures