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_13

Specification Description

The UAS's position will be bounded within a circle of radius of MAX_RECEIVER_DIST

Signals Required

PosN, PosE, PosD

Boolean Conversion of Signals to Atomic Inputs 

PosMag = √(PosN² + PosE² + PosD²)
PosMag_leq_MAX: PosMag ≤ MAX_RECIEVER_DIST

MLTL Specification

☐[0,M] (PosMag_leq_Max)

Fault Explanation

Position magnitude is exceeding receiver distance

Additional Notes

Figures

Figure 1: Position distance from reciever.
Figure 2: R2U2's output of OR_UAS_13, showing that the distance never exceeded bounds.
Figure 3: Injected fault into position distance, exceeding the upper bound.
Figure 4: R2U2's output, showing the fault was detected and R2U2 returned false.