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

IS_UAS_4

Specification Description

The vertical velocity measurement difference from the GPS and the IMU should be less than ERROR_VEL.

Signals Required

VelD (GPS), AccD (IMU)

Boolean Conversion of Signals to Atomic Inputs 

VelD_lt_PrevVA_plus_Error: VelD < PREV_VelD + PREV_AccD + ERROR_VEL
VelD_gt_PrevVA_minus_Error: VelD > PREV_VelD + PREV_AccD - ERROR_VEL

MLTL Specification

¬☐[0,3] ¬(VelD_lt_PrevVA_plus_Error ∧ VelN_gt_PrevVA_minus_Error)

Fault Explanation

The error of the vertical velocity between the GPS and the IMU is out of bounds.

Additional Notes

Acceleration component is multiplied by change in time, but for the Vapor dt=1

Figures

Figure 1: Display of the relationship between the Acceleration Down and the Velocity Down.
Figure 2: R2U2's output of IS_UAS_4, showing that the Velocity Down and Acceleration Down follow their constrained relationship.
Figure 3: Fault injected into the relationship between the Accelration Down and Velocity Down. Velocity is constantly, rapidly changing, when Acceleration in still zero.
Figure 4: R2U2's output return's a false reading during the time the fault is injected, showing that R2U2 is able to detect faults.