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

SB_GCS_2

Specification Description

All wpLon will be bounded between -180 and 180 degrees

Signals Required

wpLon

Boolean Conversion of Signals to Atomic Inputs

wpLon_leq_MaxLonUB: wpLon ≤ MaxLonUB
wpLon_geq_MinLonLB: wpLon ≥ MinLonLB

MLTL Specification

¬☐[0,M] ¬(wpLon_leq_MaxLonUB ∧ wpLon_geq_MinLonLB)

Fault Explanation

Longitude is outside of path between way points

Additional Notes

All Latitude and Longitude values should be actual Earth locations

Figures

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