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_7

Specification Description

The TempE1 of the UAS will be bounded between TEMPE1_OR_MIN and TEMPE1_OR_MAX, but if it is not, allow 3 timesteps to recover.

Signals Required

TempE1

Boolean Conversion of Signals to Atomic Inputs

TempE1_leq_MAX: Temp ≤ TempE1_OR_MAX
TempE1_geq_MIN: Temp ≥ TempE1_OR_MIN

MLTL Specificaiton

¬☐[0,3] ¬(TempE1_leq_MIN ∧ TempE1_geq_MIN)

Fault Explanation

Engine One temperature is exceeding flight bounds

Additional Notes

TempE1_OR_MIN and TempE1_OR_MAX based on acceptable flight conditions (primarily dependent on battery operating conditions)

Figure

Figure 1: Graph of the temperature of Engine One onboard the Vapor 55.
Figure 2: R2U2's output of OR_UAS_7, showing that the temperature stayed inside the bounds.
Figure 3: Fault injected into the temperature reading, exceeding the upper bound.
Figure 4: R2U2's output, detecting the injected fault and returning false during that timestep.