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_5

Specification Description

The Altitude (Alt in AGL) will be bounded between 0 and ALT_SENS_MAX, but if it is not, allow 3 timesteps to recover

Signals Required

Alt

Boolean Conversion of Signals to Atomic Inputs 

Alt_geq_0: Alt ≥ 0.0
Alt_leq_MAX: Alt ≤ ALT_SENS_MAX

MLTL Specification

¬☐[0,3] ¬(Alt_geq_0 ∧ Alt_leq_MAX)

Fault Explanation

Altitude has been outside of physical possiblity for too much time

Additional Notes

ALT_SENS_MAX would be obtained from barometer datasheet. Allows for oscillation in data

Figures

Figure 1: Altitude of the Vapor 55.
Figure 2: R2U2's output of SB_UAS_5, showing that the Altitude never exceeded the sensors bounds.
Figure 3: An injected fault into the altitude.
Figure 4: R2U2's output of Fig. 3, showing that it was able to detect the injected fault.