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_4

Specification Description

All Lon will bounded between -180 and 180 degrees

Signals Required

Lon

Boolean Conversion of Signals to Atomic Inputs

Lon_leq_MaxLonUB: Lon ≤ MaxLonUB
Lon_geq_MinLonLB: Lon ≥ MinLonLB

MLTL Specification

¬☐[0,M] ¬(Lon_leq_MaxLonUB ∧ Lon_geq_MinLonLB)

Fault Explanation

Longitude is outside of physical possibility

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