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_GCS_11

Specification Description

The altitude reference waypoint (wpAlt) that any UASs is flying towars will be bounded between 0.0 and ALT_UB

Signals Required

wpAlt

Boolean Conversion of Signals to Atomic Inputs 

wpAlt_leq_AltUB: wpAlt ≤ AltUB
wpAlt_geq_0 : wpAlt ≥ 0.0

MLTL Specificaiton

wpAlt_leq_AltUB ∧ wpAlt_geq_0

Fault Explanation

Any reference waypoint should be within the UTM's airspace

Additional Notes

Figures

Figure 1: Caption
Figure 2: Caption
Figure 3: Caption
Figure 4: Caption
Figure 5: Caption