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

SB_UAS_14

Specification Description

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

Signals Required

TempE1

Boolean Conversion of Signals to Atomic Inputs 

TempE1_leq_MAX: TempE1 ≤ TempE1_SENS_MAX
TempE1_geq_MIN: TempE1 ≥ TempE1_SENS_MIN

MLTL Specification

☐[0,M] (TempE1_leq_MAX ∧ TempE1_geq_MIN)

Fault Explanation

Engine One temperature is not within operating range

Additional Notes

TEMPE1_SENS_MAX and TEMPE1_SENS_MIN would be obtained from sensor data sheet. Allows for data oscillation

Figure

Figure 1: Engine One Temperature of the Vapor 55.
Figure 2: R2U2's output of SB_UAS_14, showing the temperature never exceed's the possible bounds.
Figure 3: An injected fault into that puts the temperature above the upper bound.
Figure 4: R2U2's output of Fig. 3, showing that R2U2 is able to detect the injected fault.