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_3

Specification Description

The Pitch measurement will be bounded between -45 and 45 degrees, but if it exceeds it, allow 3 timesteps to recover.

Signals Required

Pitch

Boolean Conversion of Signals to Atomic Inputs 

Pitch_geq_45: Pitch ≥ -45
Pitch_leq_45: Pitch ≤ 45

MLTL Specification

¬☐[0,3] ¬(Pitch_geq_45 ∧ Pitch_leq_45)

Fault Explanation

Pitch is exceeding flight bounds

Additional Notes

45 degrees is highly conservative

Figures

Figure 1: Pitch of the Vapor 55 with bounds.
Figure 2: R2U2's output of OR_UAS_3, showing that the pitch never exceeding it's bounds.
Figure 3: Injected fault into pitch, where it exceeds the upper bound.
Figure 4: R2U2's output with the injected fault, showing that R2U2 caught the error.