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

OR_UAS_12

Specification Description

The magnitude of the individual position components (PosN, PosE, PosD) will be bounded between 0 and DIST_OR_MAX, but if it is not, allow 3 timesteps to recover.

Signals Required

PosN, PosE, PosD

Boolean Conversion of Signals to Atomic Inputs 

PosMag = √(PosN² + PosE² + PosD²)
PosMag_lt_MAX: PosMag < DIST_OR_MAX

MLTL Specification

¬☐[0,3] ¬(PosMag_lt_MAX)

Fault Explanation

Position magnitude is exceeding flight bounds

Additional Notes

DIST_OR_MAX given in data sheet as 8 km

Figures

Figure 1: Distance the Vapor is from the GCS.
Figure 2: R2U2's output of OR_UAS_12, showing that the Vapor never exceeded the flight bounds.
Figure 3: Injected fault, so the distance exceeds the upper bound.
Figure 4: R2U2's output showing it deteced the injected fault and returned false.