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_17

Specification Description

The magnitude of acceleration vector (AccN, AccE, AccD) will be bounded between 0 and ACC_SENS_MAX, but if it is not, allow 3 timesteps to recover

Signals Required

AccN, AccE, AccD

Boolean Conversion of Signals to Atomic Inputs 

Acc_Mag = √(AccN² + AccE² + AccD²)
Acc_Mag_leq_MAX: Acc_Mag ≤ ACC_SENSE_MAX
Acc_Mag_geq_0: Acc_Mag ≥ 0

MLTL Specification

¬☐[0,3] ¬(Acc_Mag_leq_MAX ∧ Acc_Mag_geq_0)

Fault Explanation

Acceleration is not physically possible

Additional Notes

ACC_SENS_MAX equal to ~2G (20 m/s²) as conservative value

Figures

Figure 1: Acceleration Magnitude of Vapor 55.
Figure 2: R2U2's output of SB_UAS_17, showing that the acceleration magnitude never exceeded the bounds.
Figure 3: An injected fault into the acceleration's magnitude.
Figure 4: R2U2's output of Fig. 3, showing the R2U2 was able to detect the injected fault.