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

PM_UAS_1

Specification Description

When the VelN is positive and not small (>0.25m/s), the change in Lat shall be greater than 0 at all instances (in the northern hemisphere). The opposite shall be true when VelN is negative and not small (<0.25m/s).

Signals Required

VelN, Lat

Boolean Conversion of Signals to Atomic Inputs

DeltaLat = Lat - PREV_LAT
VelN_gt_0.25: VelN > 0.25
VelN_lt_0.25: VelN < -0.25
DeltaLab_gt_0: DeltaLat > 0
DeltaLat_lt_0: DeltaLat < 0

MLTL Specification

☐[0,M] [(VelN_gt_0.25 ∧ DeltaLab_gt_0) ∨ (VelN_lt_0.25 ∧ DeltaLat_lt_0)]

Fault Explanation

There is no change in Latitude due to the Velocity North, where there should be.

Additional Notes

Need magnitude of VelN to be small so that a DeltaLat should be non 0. This accounts for some of minor disturbances that might occur when stationary.

Figures