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_2

Specification Description

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

Signals Required

VelN (GPS), AccN (IMU)

Boolean Conversion of Signals to Atomic Inputs 

VelN_lt_PrevVA_plus_Error: VelN < PREV_VelN + PREV_AccN + ERROR_VEL
VelN_gt_PrevVA_minus_Error: VelN > PREV_VelN +PREV_AccN - ERROR_VEL

MLTL Specification

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

Fault Explanation

The error of the northern 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 North and the Velocity North.
Figure 2: R2U2's output of IS_UAS_2, showing that the Velocity North and Acceleration North follow their constrained relationship.
Figure 3: Fault injected into the relationship between the Accelration North and Velocity North. 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.