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_15

Specification Description

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

Signals Required

TempE2

Boolean Conversion of Signals to Atomic Inputs 

TempE2_leq_MAX: TempE2 ≤ TEMPE2_SENS_MAX
TempE2_geq_MIN: TempE2 ≥ TEMPE2_SENS_MIN

MLTL Specification

☐[0,M] (TempE2_leq_MAX ∧ TempE2_geq_MIN)

Fault Explanation

Engine Two temperature is not within operating range

Additional Notes

TEMPE2_SENS_MAX and TEMPE2_SENS_MIN would be obtained from sensor data sheet. Allows for data oscillation

Figures

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