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_16

Specification Description

The Pres of the UAS will be bounded between 0 and PRES_SENS_MAX at all instances

Signals Required

Pres

Boolean Conversion of Signals to Atomic Inputs 

Pres_leq_MAX: Pres ≤ PRES_SENS_MAX
Pres_geq_0: Pres ≥ 0

MLTL Specification

☐[0,M] (Pres_leq_MAX ∧ Pres_geq_0)

Fault Explanation

Pressure is not physically possible

Additional Notes

PRES_SENS_MAX would be obtained from barometer data sheet

Figure

Figure 1: Pressure from barometer, with bounds barometer is able to measure.
Figure 2: R2U2's output, showing that SB_UAS_16 never exceeds the bounds.
Figure 3: An injected fault where the pressure exceeds the upper bound.
Figure 4: R2U2's output showing that the fault was detected.