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_3

Specification Description

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

Signals Required

VelE (GPS), AccE (IMU)

Boolean Conversion of Signals to Atomic Inputs 

VelE_lt_PrevVA_plus_Error: VelE < PREV_VelE + PREV_AccE + ERROR_VEL 
VelE_gt_PrevVA_minus_Error: VelE > PREV_VelE +PREV_AccE - ERROR_VEL

MLTL Specification

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

Fault Explanation

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