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_UAS_10

Specification Description

The magnitude of the horizontal velocity components (VelN, VelE) will be bounded between 0 and VELH_OR_MAX at all instances.

Signals Required

VelN, VelE

Boolean Conversion of Signals to Atomic Inputs 

VelH_Mag = √(VelN² + VelE²)
VelH_Mag_leq_MAX: VelH_Mag ≤ VELH_OR_MAX
VelH_Mag_geq_0: VelH_Mag ≥ 0

MLTL Specification

¬☐[0,3] ¬(VelH_Mag_leq_MAX ∧ VelH_Mag_geq_0)

Fault Explanation

Horizontal velocity is exceeding flight bounds

Additional Notes

VELH_OR_MAX is maximum horizontal speed (given in data sheet as 15 m/s)

Figures

Figure 1: Graph displaying the Horizontal Velocity and bounds.
Figure 2: R2U2's output of OR_UAS_10, showing that the Horizontal Velocity stayed within bounds the entire time.
Figure 3: Fault injected into the horizontal velocity where it exceeds the maximum bound.
Figure 4: R2U2's output showing that it is able to detect a fault when the horizontal velocity exceeds it's bounds.