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_13

Specification Description

The Temp of the UAS will be bounded between TEMP_SENS_MIN and TEMP_SENS_MAX, but if it is not, allow 3 timesteps to recover

Signals Required

Temp

Boolean Conversion of Signals to Atomic Inputs 

Temp_leq_MAX: Temp ≤ Temp_SENS_MAX
Temp_geq_MIN: Temp ≥ Temp_SENS_MIN

MLTL Specification

☐[0,M] (Temp_leq_MAX ∧ Temp_geq_MIN)

Fault Explanation

Ambient temperature is not within operating range

Additional Notes

TEMP_SENS_MAX and TEMP_SENS_MIN would be obtained from sensor data sheet. Allows for data oscillation

Figures

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