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_8

Specificaiton Description

The TempE2 of the UAS will be bounded between TempE2_OR_MIN and TempE2_OR_MAX, but if it is not, allow 3 timesteps to recover.

Signals Required

TempE2

Boolean Conversion of Signals to Atomic Inputs 

TempE2_leq_MAX: Temp ≤ TempE2_OR_MAX
TempE2_geq_MIN: Temp ≥ TempE2_OR_MIN

MLTL Specificaiton

¬☐[0,3] ¬(TempE2_leq_MIN ∧ TempE2_geq_MIN)

Fault Explanation

Engine Two temperature is exceeding flight bounds

Additional Notes

TempE2_OR_MIN and TempE2_OR_MAX based on acceptable flight conditions (primarily dependent on battery operating conditions)

Figures

Figure 1: Graph of the temperature of Engine Two onboard the Vapor 55.
Figure 2: R2U2's output of OR_UAS_8, 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.