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_6

Specification Description

The Altitude (Alt in AGL) will be bounded between 0 and ALT_SENS_MAX at all instances

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,M] (Alt_geq_0 ∧ Alt_leq_MAX)

Fault Explanation

Altitude is outside of physical possiblity

Additional Notes

ALT_SENS_MAX would be obtained from barometer datasheet.

Figures

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