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_9

Specificaiton Description

The Pres of the UAS will be bounded between PRES_OR_MIN and PRES_OR_MAX, but if it is not, allow 3 timesteps to recover.

Signals Required

Pres

Boolean Conversion of Signals to Atomic Inputs 

Pres_leq_MAX: Pres ≤ PRES_OR_MAX
Pres_geq_MIN: Pres ≥ PRES_OR_MIN

MLTL Specificaiton

¬☐[0,3] ¬(Pres_leq_MAX ∧ Pres_geq_MIN)

Fault Explanation

Pressure is exceeding flight bounds

Additional Notes

PRES_OR_MIN and PRES_OR_MAX based on pressures at expected flight altitudes and aircraft MSL ceiling

Figures

Figure 1: Pressure read by barometer during the Vapor 55's flight.
Figure 2: R2U2's output of OR_UAS_9, confirming that the pressure never exceeds it's bounds.
Figure 3: Fault injected into the pressure reading, so that it exceeds the upper bound.
Figure 4: R2U2's output showing that it was able to detect the injected fault.